[STATEMENT]
theorem HPhase1or2ReadThen_HInv4c:
  "\<lbrakk> HPhase1or2ReadThen s s' p d r; HInv4c s q\<rbrakk>
          \<Longrightarrow> HInv4c s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HPhase1or2ReadThen s s' p d r; HInv4c s q\<rbrakk> \<Longrightarrow> HInv4c s' q
[PROOF STEP]
by(blast dest: HPhase1or2ReadThen_HInv4c_p
                 HPhase1or2ReadThen_HInv4c_q)