[STATEMENT]
lemma valid_refs_inv_eq_imp:
  "eq_imp (\<lambda>(m', r'). (\<lambda>s. roots (s (mutator m'))) \<^bold>\<otimes> (\<lambda>s. ghost_honorary_root (s (mutator m'))) \<^bold>\<otimes> (\<lambda>s. map_option obj_fields (sys_heap s r')) \<^bold>\<otimes> tso_pending_mutate (mutator m') \<^bold>\<otimes> (\<lambda>s. \<Union>p. WL p s))
          valid_refs_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>(m', r') s. (roots (s (mutator m')), ghost_honorary_root (s (mutator m')), map_option obj_fields (sys_heap s r'), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m') s), \<Union>p. WL p s)) valid_refs_inv
[PROOF STEP]
apply (clarsimp simp: eq_imp_def valid_refs_inv_def grey_reachable_def all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa s \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa s \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
[PROOF STEP]
apply (subgoal_tac "\<forall>r'. valid_ref r' s \<longleftrightarrow> valid_ref r' s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa s \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
[PROOF STEP]
apply (subgoal_tac "\<forall>r'. \<Union>(ran ` obj_fields ` set_option (sys_heap s r')) = \<Union>(ran ` obj_fields ` set_option (sys_heap s' r'))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa s \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
[PROOF STEP]
apply (subst eq_impD[OF mut_m.reachable_eq_imp])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'15 s s' (mutator x)), ghost_honorary_root (?s'15 s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'15 s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'15 s s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'15 s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 4. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'15 s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa s \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'15 s s' (mutator x)), ghost_honorary_root (?s'15 s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'15 s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'15 s s')))
[PROOF STEP]
apply (subst eq_impD[OF grey_eq_imp])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p (?s'18 s s')))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'a18 s s' s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa (?s'18 s s') \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 4. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 5. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'a18 s s' s s' (mutator x)), ghost_honorary_root (?s'a18 s s' s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'a18 s s' s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'a18 s s' s s')))
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'a18 s s' s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa (?s'18 s s') \<and> (xa reaches x) s) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'a18 s s' s s' (mutator x)), ghost_honorary_root (?s'a18 s s' s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'a18 s s' s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'a18 s s' s s')))
 5. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p (?s'18 s s')))
[PROOF STEP]
apply (subst eq_impD[OF reaches_eq_imp])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'23 s s') x))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'aa23 s s' s s' s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa (?s'a23 s s' s s') \<and> (xa reaches x) (?s'23 s s')) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 4. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 5. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'a18 s s' s s' (mutator x)), ghost_honorary_root (?s'a18 s s' s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'a18 s s' s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'a18 s s' s s')))
 6. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p (?s'a23 s s' s s')))
flex-flex pairs:
\<lambda>s s'. ?s'aa23 s s' s s' s s' \<equiv>\<^sup>? \<lambda>s s'. ?s'a18 s s' s s'
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> ((\<forall>x xa. mut_m.reachable x xa (?s'aa23 s s' s s' s s') \<longrightarrow> obj_at (\<lambda>s. True) xa s) \<and> (\<forall>x. (\<exists>xa. grey xa (?s'a23 s s' s s') \<and> (xa reaches x) (?s'23 s s')) \<longrightarrow> obj_at (\<lambda>s. True) x s)) = ((\<forall>x xa. mut_m.reachable x xa s' \<longrightarrow> obj_at (\<lambda>s. True) xa s') \<and> (\<forall>x. (\<exists>xa. grey xa s' \<and> (xa reaches x) s') \<longrightarrow> obj_at (\<lambda>s. True) x s'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 3. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (?s'a18 s s' s s' (mutator x)), ghost_honorary_root (?s'a18 s s' s s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'a18 s s' s s') xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) (?s'a18 s s' s s')))
 5. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p (?s'a23 s s' s s')))
 6. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'23 s s') x))
flex-flex pairs:
\<lambda>s s'. ?s'aa23 s s' s s' s s' \<equiv>\<^sup>? \<lambda>s s'. ?s'a18 s s' s s'
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'\<rbrakk> \<Longrightarrow> \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))
 2. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 3. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (s' (mutator x)), ghost_honorary_root (s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s' xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s'))
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p s'))
 5. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply (metis option.set_map)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'
 2. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (s' (mutator x)), ghost_honorary_root (s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s' xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s'))
 3. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p s'))
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s' r'. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s')\<rbrakk> \<Longrightarrow> (sys_heap s r' = None \<longrightarrow> sys_heap s' r' = None) \<and> ((\<exists>obj. sys_heap s r' = Some obj) \<longrightarrow> (\<exists>y. sys_heap s' r' = Some y))
 2. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (s' (mutator x)), ghost_honorary_root (s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s' xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s'))
 3. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p s'))
 4. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply (metis (no_types, opaque_lifting) None_eq_map_option_iff option.exhaust)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>xa. (roots (s (mutator x)), ghost_honorary_root (s (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s)) = (roots (s' (mutator x)), ghost_honorary_root (s' (mutator x)), \<Union> (ran ` obj_fields ` set_option (sys_heap s' xa)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator x) s'))
 2. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p s'))
 3. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. (xa \<in> (\<Union>p. WL p s)) = (xa \<in> (\<Union>p. WL p s'))
 2. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa x. \<lbrakk>\<forall>a. roots (s (mutator a)) = roots (s' (mutator a)); \<forall>a. ghost_honorary_root (s (mutator a)) = ghost_honorary_root (s' (mutator a)); \<forall>b. map_option obj_fields (sys_heap s b) = map_option obj_fields (sys_heap s' b); \<forall>a. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator a) s'); (\<Union>p. WL p s) = (\<Union>p. WL p s'); \<forall>r'. obj_at (\<lambda>s. True) r' s = obj_at (\<lambda>s. True) r' s'; \<forall>r'. \<Union> (ran ` obj_fields ` set_option (sys_heap s r')) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' r'))\<rbrakk> \<Longrightarrow> \<forall>x. \<Union> (ran ` obj_fields ` set_option (sys_heap s x)) = \<Union> (ran ` obj_fields ` set_option (sys_heap s' x))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma valid_refs_invD[elim]:
  "\<lbrakk> x \<in> mut_m.mut_roots m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref y s"
  "\<lbrakk> x \<in> mut_m.mut_roots m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj"
  "\<lbrakk> x \<in> mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref y s"
  "\<lbrakk> x \<in> mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj"
  "\<lbrakk> w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> store_refs w; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref y s"
  "\<lbrakk> w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> store_refs w; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj"
  "\<lbrakk> grey x s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref y s"
  "\<lbrakk> mut_m.reachable m x s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref x s"
  "\<lbrakk> mut_m.reachable m x s; valid_refs_inv s \<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s x = Some obj"
  "\<lbrakk> x \<in> mut_m.mut_ghost_honorary_root m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref y s"
  "\<lbrakk> x \<in> mut_m.mut_ghost_honorary_root m s; (x reaches y) s; valid_refs_inv s \<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<lbrakk>x \<in> roots (s (mutator m)); (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s) &&& (\<lbrakk>x \<in> roots (s (mutator m)); (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj)) &&& (\<lbrakk>x \<in> mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s) &&& (\<lbrakk>x \<in> mut_m.tso_store_refs m s; (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj) &&& (\<lbrakk>w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> store_refs w; (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s)) &&& ((\<lbrakk>w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> store_refs w; (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj) &&& (\<lbrakk>grey x s; (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s) &&& (\<lbrakk>mut_m.reachable m x s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) x s)) &&& (\<lbrakk>mut_m.reachable m x s; valid_refs_inv s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s x = Some obj) &&& (\<lbrakk>x \<in> ghost_honorary_root (s (mutator m)); (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) y s) &&& (\<lbrakk>x \<in> ghost_honorary_root (s (mutator m)); (x reaches y) s; valid_refs_inv s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj)
[PROOF STEP]
apply (simp_all add: valid_refs_inv_def grey_reachable_def mut_m.reachable_def mut_m.tso_store_refs_def
              split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); x \<in> roots (s (mutator m)); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 2. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); x \<in> roots (s (mutator m)); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj
 3. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 4. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); \<exists>xa\<in>set (sys_mem_store_buffers (mutator m) s). x \<in> (case xa of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj
 5. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 6. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); w \<in> set (sys_mem_store_buffers (mutator m) s); x \<in> (case w of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {}); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj
 7. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); grey x s; (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 8. \<And>xa. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); xa \<in> roots (s (mutator m)) \<or> xa \<in> ghost_honorary_root (s (mutator m)) \<or> (\<exists>x\<in>set (sys_mem_store_buffers (mutator m) s). xa \<in> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})); (xa reaches x) s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s x = Some obj
 9. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); x \<in> ghost_honorary_root (s (mutator m)); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>ya. sys_heap s y = Some ya
 10. \<lbrakk>\<forall>x xa. (\<exists>y. sys_heap s xa = Some y) \<or> (\<forall>xb. xb \<notin> roots (s (mutator x)) \<and> xb \<notin> ghost_honorary_root (s (mutator x)) \<and> (\<forall>x\<in>set (sys_mem_store_buffers (mutator x) s). xb \<notin> (case x of mw_Mutate r f r' \<Rightarrow> insert r (set_option r') | mw_Mutate_Payload r f pl \<Rightarrow> {r} | _ \<Rightarrow> {})) \<or> \<not> (xb reaches xa) s) \<and> (\<forall>x. grey x s \<longrightarrow> \<not> (x reaches xa) s); x \<in> ghost_honorary_root (s (mutator m)); (x reaches y) s\<rbrakk> \<Longrightarrow> \<exists>obj. sys_heap s y = Some obj
[PROOF STEP]
apply blast+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma reachable_snapshot_invI[intro]:
  "(\<And>y. reachable y s \<Longrightarrow> in_snapshot y s) \<Longrightarrow> reachable_snapshot_inv s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. reachable y s \<Longrightarrow> in_snapshot y s) \<Longrightarrow> reachable_snapshot_inv s
[PROOF STEP]
by (simp add: reachable_snapshot_inv_def)


[STATEMENT]
lemma reachable_snapshot_inv_eq_imp:
  "eq_imp (\<lambda>r'. mut_roots \<^bold>\<otimes> mut_ghost_honorary_root \<^bold>\<otimes> (\<lambda>s. r' \<in> (\<Union>p. WL p s)) \<^bold>\<otimes> sys_fM
            \<^bold>\<otimes> (\<lambda>s. \<Union>(ran ` obj_fields ` set_option (sys_heap s r'))) \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r'))
            \<^bold>\<otimes> tso_pending_mutate (mutator m))
          reachable_snapshot_inv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (mut_roots s, mut_ghost_honorary_root s, r' \<in> (\<Union>p. WL p s), sys_fM s, \<Union> (ran ` obj_fields ` set_option (sys_heap s r')), map_option obj_mark (sys_heap s r'), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s))) reachable_snapshot_inv
[PROOF STEP]
unfolding eq_imp_def mut_m.reachable_snapshot_inv_def in_snapshot_def grey_protects_white_def black_def grey_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (mut_roots s, mut_ghost_honorary_root s, x \<in> (\<Union>p. WL p s), sys_fM s, \<Union> (ran ` obj_fields ` set_option (sys_heap s x)), map_option obj_mark (sys_heap s x), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s)) = (mut_roots s', mut_ghost_honorary_root s', x \<in> (\<Union>p. WL p s'), sys_fM s', \<Union> (ran ` obj_fields ` set_option (sys_heap s' x)), map_option obj_mark (sys_heap s' x), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'))) \<longrightarrow> (\<forall>x. reachable x s \<longrightarrow> marked x s \<and> (\<nexists>xa. x \<in> WL xa s) \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s) \<and> (xa has_white_path_to x) s)) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<nexists>xa. x \<in> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply (clarsimp simp: all_conj_distrib)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s)) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply (rename_tac s s')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s)) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply (subst (1) eq_impD[OF has_white_path_to_eq_imp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' xa x. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>x. (sys_fM s, \<Union> (ran ` obj_fields ` set_option (sys_heap s x)), map_option obj_mark (sys_heap s x)) = (sys_fM (?s'22 s s'), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'22 s s') x)), map_option obj_mark (sys_heap (?s'22 s s') x))
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) (?s'22 s s'))) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s')) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply (subst eq_impD[OF reachable_eq_imp])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' x. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>x. (mut_roots s, mut_ghost_honorary_root s, \<Union> (ran ` obj_fields ` set_option (sys_heap s x)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s)) = (mut_roots (?s'40 s s'), mut_ghost_honorary_root (?s'40 s s'), \<Union> (ran ` obj_fields ` set_option (sys_heap (?s'40 s s') x)), filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) (?s'40 s s')))
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x (?s'40 s s') \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s')) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s' \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s')) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
[PROOF STEP]
apply (subgoal_tac "\<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<longleftrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'\<rbrakk> \<Longrightarrow> (\<forall>x. reachable x s' \<longrightarrow> obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s')) = (\<forall>x. reachable x s' \<longrightarrow> marked x s' \<and> (\<forall>xa. x \<notin> WL xa s') \<or> (\<exists>xa. (\<exists>x. xa \<in> WL x s') \<and> (xa has_white_path_to x) s'))
 2. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> \<forall>x. obj_at (\<lambda>obj. obj_mark obj = sys_fM s') x s = marked x s'
[PROOF STEP]
apply (clarsimp split: obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; \<forall>x. (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); sys_fM s = sys_fM s'; \<forall>x. (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (drule_tac x=x in spec)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); (\<Union>a\<in>set_option (sys_heap s x). ran (obj_fields a)) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> obj_mark obj = (\<not> sys_fM s'))) \<and> (\<forall>obj. sys_heap s x = Some obj \<longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark obj = (\<not> sys_fM s')) \<and> (\<forall>obja. sys_heap s' x = Some obja \<longrightarrow> (obj_mark obj = sys_fM s') = (obj_mark obja = sys_fM s')))
[PROOF STEP]
apply (case_tac "sys_heap s x", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x a. \<lbrakk>mut_roots s = mut_roots s'; mut_ghost_honorary_root s = mut_ghost_honorary_root s'; sys_fM s = sys_fM s'; filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s'); (\<exists>xa. x \<in> WL xa s) = (\<exists>xa. x \<in> WL xa s'); ran (obj_fields a) = (\<Union>a\<in>set_option (sys_heap s' x). ran (obj_fields a)); Some (obj_mark a) = map_option obj_mark (sys_heap s' x); sys_heap s x = Some a\<rbrakk> \<Longrightarrow> (sys_heap s' x = None \<longrightarrow> obj_mark a = (\<not> sys_fM s')) \<and> (\<forall>obj. sys_heap s' x = Some obj \<longrightarrow> (obj_mark a = sys_fM s') = (obj_mark obj = sys_fM s'))
[PROOF STEP]
apply (case_tac "sys_heap s' x", simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma in_snapshotI[intro]:
  "black r s \<Longrightarrow> in_snapshot r s"
  "grey r s \<Longrightarrow> in_snapshot r s"
  "\<lbrakk> white w s; (g grey_protects_white w) s \<rbrakk> \<Longrightarrow> in_snapshot w s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (black r s \<Longrightarrow> in_snapshot r s) &&& (grey r s \<Longrightarrow> in_snapshot r s) &&& (\<lbrakk>white w s; (g grey_protects_white w) s\<rbrakk> \<Longrightarrow> in_snapshot w s)
[PROOF STEP]
by (auto simp: in_snapshot_def)


[STATEMENT]
lemma \<comment> \<open>Sanity\<close>
  "in_snapshot r s \<Longrightarrow> black r s \<or> grey r s \<or> white r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. in_snapshot r s \<Longrightarrow> black r s \<or> grey r s \<or> white r s
[PROOF STEP]
by (auto simp: in_snapshot_def)


[STATEMENT]
lemma in_snapshot_valid_ref:
  "\<lbrakk> in_snapshot r s; valid_refs_inv s \<rbrakk> \<Longrightarrow> valid_ref r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>in_snapshot r s; valid_refs_inv s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>s. True) r s
[PROOF STEP]
by (metis blackD(1) grey_protects_whiteD grey_protects_white_reaches in_snapshot_def obj_at_cong obj_at_def option.case(2) valid_refs_invD(7))


[STATEMENT]
lemma reachableI2[intro]:
  "x \<in> mut_m.mut_ghost_honorary_root m s \<Longrightarrow> mut_m.reachable m x s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> mut_m.reachable m x s
[PROOF STEP]
unfolding mut_m.reachable_def reaches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> ghost_honorary_root (s (mutator m)) \<Longrightarrow> \<exists>xa. xa \<in> roots (s (mutator m)) \<union> ghost_honorary_root (s (mutator m)) \<union> mut_m.tso_store_refs m s \<and> (\<lambda>x y. (x points_to y) s)\<^sup>*\<^sup>* xa x
[PROOF STEP]
by blast


[STATEMENT]
lemma tso_pending_mw_mutate_cong:
  "\<lbrakk> filter is_mw_Mutate (sys_mem_store_buffers p s) = filter is_mw_Mutate (sys_mem_store_buffers p s');
     \<And>r f r'. P r f r' \<longleftrightarrow> Q r f r' \<rbrakk>
     \<Longrightarrow> (\<forall>r f r'. mw_Mutate r f r' \<in> set (sys_mem_store_buffers p s)  \<longrightarrow> P r f r')
     \<longleftrightarrow> (\<forall>r f r'. mw_Mutate r f r' \<in> set (sys_mem_store_buffers p s') \<longrightarrow> Q r f r')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>filter is_mw_Mutate (sys_mem_store_buffers p s) = filter is_mw_Mutate (sys_mem_store_buffers p s'); \<And>r f r'. P r f r' = Q r f r'\<rbrakk> \<Longrightarrow> (\<forall>r f r'. mw_Mutate r f r' \<in> set (sys_mem_store_buffers p s) \<longrightarrow> P r f r') = (\<forall>r f r'. mw_Mutate r f r' \<in> set (sys_mem_store_buffers p s') \<longrightarrow> Q r f r')
[PROOF STEP]
by (intro iff_allI) (auto dest!: arg_cong[where f=set])


[STATEMENT]
lemma (in mut_m) marked_insertions_eq_imp:
  "eq_imp (\<lambda>r'. sys_fM \<^bold>\<otimes> (\<lambda>s. map_option obj_mark (sys_heap s r')) \<^bold>\<otimes> tso_pending_mw_mutate (mutator m))
          marked_insertions"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq_imp (\<lambda>r' s. (sys_fM s, map_option obj_mark (sys_heap s r'), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s))) marked_insertions
[PROOF STEP]
unfolding eq_imp_def marked_insertions_def obj_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (\<forall>x. (sys_fM s, map_option obj_mark (sys_heap s x), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s)) = (sys_fM s', map_option obj_mark (sys_heap s' x), filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s'))) \<longrightarrow> (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x of mw_Mutate r f None \<Rightarrow> True | mw_Mutate r f (Some r') \<Rightarrow> case sys_heap s r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s | _ \<Rightarrow> True)) = (\<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x of mw_Mutate r f None \<Rightarrow> True | mw_Mutate r f (Some r') \<Rightarrow> case sys_heap s' r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s' | _ \<Rightarrow> True))
[PROOF STEP]
apply (clarsimp split: mem_store_action.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x); filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s) = filter is_mw_Mutate (sys_mem_store_buffers (mutator m) s')\<rbrakk> \<Longrightarrow> (\<forall>x21 x22 x23. mw_Mutate x21 x22 x23 \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> (case x23 of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s)) = (\<forall>x21 x22 x23. mw_Mutate x21 x22 x23 \<in> set (sys_mem_store_buffers (mutator m) s') \<longrightarrow> (case x23 of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s' r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s'))
[PROOF STEP]
apply (erule tso_pending_mw_mutate_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x21 x22 x23. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (case x23 of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s) = (case x23 of None \<Rightarrow> True | Some r' \<Rightarrow> case sys_heap s' r' of None \<Rightarrow> False | Some obj \<Rightarrow> obj_mark obj = sys_fM s')
[PROOF STEP]
apply (clarsimp split: option.splits obj_at_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' x23 x2. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x2 = None \<longrightarrow> (\<forall>x2a. sys_heap s' x2 = Some x2a \<longrightarrow> x23 = Some x2 \<longrightarrow> obj_mark x2a = (\<not> sys_fM s'))) \<and> (\<forall>x2a. sys_heap s x2 = Some x2a \<longrightarrow> (sys_heap s' x2 = None \<longrightarrow> x23 = Some x2 \<longrightarrow> obj_mark x2a = (\<not> sys_fM s')) \<and> (\<forall>x2b. sys_heap s' x2 = Some x2b \<longrightarrow> x23 = Some x2 \<longrightarrow> (obj_mark x2a = sys_fM s') = (obj_mark x2b = sys_fM s')))
[PROOF STEP]
apply (rename_tac s s' opt x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' opt x. \<lbrakk>sys_fM s = sys_fM s'; \<forall>x. map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>x2. sys_heap s' x = Some x2 \<longrightarrow> opt = Some x \<longrightarrow> obj_mark x2 = (\<not> sys_fM s'))) \<and> (\<forall>x2. sys_heap s x = Some x2 \<longrightarrow> (sys_heap s' x = None \<longrightarrow> opt = Some x \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')) \<and> (\<forall>x2a. sys_heap s' x = Some x2a \<longrightarrow> opt = Some x \<longrightarrow> (obj_mark x2 = sys_fM s') = (obj_mark x2a = sys_fM s')))
[PROOF STEP]
apply (drule_tac x=x in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' opt x. \<lbrakk>sys_fM s = sys_fM s'; map_option obj_mark (sys_heap s x) = map_option obj_mark (sys_heap s' x)\<rbrakk> \<Longrightarrow> (sys_heap s x = None \<longrightarrow> (\<forall>x2. sys_heap s' x = Some x2 \<longrightarrow> opt = Some x \<longrightarrow> obj_mark x2 = (\<not> sys_fM s'))) \<and> (\<forall>x2. sys_heap s x = Some x2 \<longrightarrow> (sys_heap s' x = None \<longrightarrow> opt = Some x \<longrightarrow> obj_mark x2 = (\<not> sys_fM s')) \<and> (\<forall>x2a. sys_heap s' x = Some x2a \<longrightarrow> opt = Some x \<longrightarrow> (obj_mark x2 = sys_fM s') = (obj_mark x2a = sys_fM s')))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma marked_insertionD[elim!]:
  "\<lbrakk> sys_mem_store_buffers (mutator m) s = mw_Mutate r f (Some r') # ws; mut_m.marked_insertions m s \<rbrakk>
     \<Longrightarrow> marked r' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sys_mem_store_buffers (mutator m) s = mw_Mutate r f (Some r') # ws; mut_m.marked_insertions m s\<rbrakk> \<Longrightarrow> marked r' s
[PROOF STEP]
by (auto simp: mut_m.marked_insertions_def)


[STATEMENT]
lemma marked_insertions_store_buffer_empty[intro]:
  "tso_pending_mutate (mutator m) s = [] \<Longrightarrow> mut_m.marked_insertions m s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = [] \<Longrightarrow> mut_m.marked_insertions m s
[PROOF STEP]
unfolding mut_m.marked_insertions_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>s. is_mw_Mutate s \<or> is_mw_Mutate_Payload s) (sys_mem_store_buffers (mutator m) s) = [] \<Longrightarrow> \<forall>x. x \<in> set (sys_mem_store_buffers (mutator m) s) \<longrightarrow> marked_insertion x s
[PROOF STEP]
by (auto simp: filter_empty_conv split: mem_store_action.splits)