[math-fun] Dijkstra's square operator?

I'm trying to understand these slides about the fixed point fusion theorem, but the author is using some notation from Dijkstra I've never seen and don't have access to the book where it's defined. Can anyone parse this statement for me? I'm typesetting it a couple different ways, hoping one of them works for you. x∈S ⇒ b ≣ S ⊆ if b ➝∑* □ ¬b➝∑* - {x} fi x \in S \Rightarrow \equiv S \subseteq if b \to \Sigma^{*} \square \lnot b \to \Sigma^{*} - \{x\} fi Or can anyone point me at an explanation that uses a different notation? -- Mike Stay - metaweta@gmail.com http://math.ucr.edu/~mike http://reperiendi.wordpress.com