[STATEMENT]
lemma SBHWriteVolatile':
  "\<lbrakk>sb'= sb@[Write\<^sub>s\<^sub>b True a (D,f) (f \<theta>) A L R W]; ghst = (\<D>, \<O>, \<R>, \<S>); ghst' = (True, \<O>,\<R>, \<S>)\<rbrakk>
   \<Longrightarrow> 
   (Write True a (D,f) A L R W# is,\<theta>, sb, m,ghst) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h
         (is,\<theta>, sb', m,ghst')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sb' = sb @ [Write\<^sub>s\<^sub>b True a (D, f) (f \<theta>) A L R W]; ghst = (\<D>, \<O>, \<R>, \<S>); ghst' = (True, \<O>, \<R>, \<S>)\<rbrakk> \<Longrightarrow> (Write True a (D, f) A L R W # is, \<theta>, sb, m, ghst) \<rightarrow>\<^sub>s\<^sub>b\<^sub>h (is, \<theta>, sb', m, ghst')
[PROOF STEP]
by (simp add: SBHWriteVolatile)