[STATEMENT]
lemma R_abort: "abort \<le> Ref \<lceil>P\<rceil> \<lceil>Q\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abort \<le> Ref \<lceil>P\<rceil> \<lceil>Q\<rceil>
[PROOF STEP]
by (rule R2, simp)

\<comment> \<open> Sequential Composition \<close>