[STATEMENT]
lemma HPhase1or2ReadThen_HInv4a2:
  "\<lbrakk> HPhase1or2ReadThen s s' p d r; HInv4a2 s q \<rbrakk> \<Longrightarrow> HInv4a2 s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HPhase1or2ReadThen s s' p d r; HInv4a2 s q\<rbrakk> \<Longrightarrow> HInv4a2 s' q
[PROOF STEP]
by(auto simp add: Phase1or2ReadThen_def HInv4a2_def)