>>11
Ah, I think I've got it now then. Do the following seem like accurate definitions then:
[wlp(S, R)](w) = \forall x \in S(w) : R(x)
[wp(S, R)](w) = \forall x \in S(w) : R(x) \wedge S(w) \not= \emptysetEvaluating the negation of our two operations we then have:
non [wlp(S,R)](w)
= non [\forall x \in S(w) : R(x)]
= \exists x \in S(w) : non R(x)non [wp(S,R)](w)
= non [\forall x \in S(w) : R(x) \wedge S(w) \not= \emptyset]
= non [\forall x \in S(w) : R(x)] \vee non [S(w) \not= \emptyset]
= \exists x \in S(w) : R(x) \vee S(w) = \emptyset