[STATEMENT]
lemma U_F2: "Mutex \<in> {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mutex \<in> {s. \<not> p s \<and> m s = 2} \<longmapsto>w {s. m s = 3}
[PROOF STEP]
apply (cut_tac IU)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mutex \<in> Always IU \<Longrightarrow> Mutex \<in> {s. \<not> p s \<and> m s = 2} \<longmapsto>w {s. m s = 3}
[PROOF STEP]
apply (unfold Mutex_def, ensures_tac U2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done