[STATEMENT]
lemma PO_m3_step3_refines_m2_step3:
  "{R23} 
     (m2_step3 Ra A B Na Nb), (m3_step3 Ra A B Na Nb) 
   {> R23}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {R23} m2_step3 Ra A B Na Nb, m3_step3 Ra A B Na Nb {> R23}
[PROOF STEP]
by (auto simp add: PO_rhoare_defs R23_def m2_defs m3_defs intro!: R23_intros)