[STATEMENT]
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<subseteq> wp act B \<inter> awp F (B \<union> A) \<Longrightarrow> A \<subseteq> wens F act B
[PROOF STEP]
apply (simp add: wens_def wp_def awp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<subseteq> - act\<inverse> `` (- B) \<and> A - B \<subseteq> (\<Inter>x\<in>Acts F. - x\<inverse> `` (- B \<inter> - A)) \<Longrightarrow> A \<subseteq> gfp (\<lambda>X. - act\<inverse> `` (- B) \<inter> (\<Inter>x\<in>Acts F. - x\<inverse> `` (- B \<inter> - X)) \<union> B)
[PROOF STEP]
apply (rule gfp_upperbound, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done