Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:backward_vcg [2009/03/12 12:43] vkuncak |
sav08:backward_vcg [2009/03/12 12:45] vkuncak |
||
---|---|---|---|
Line 33: | Line 33: | ||
\[ | \[ | ||
\begin{array}{rl} | \begin{array}{rl} | ||
- | wp(x=e,\{(x,y) \mid Q(x,y)\}) & = \{(x,y) \mid \forall x',y'. x'=e \land y'=y \rightarrow Q(x',y') \} \\ | + | wp(x=e,\{(x,y) \mid Q(x,y)\}) & = \{(x,y) \mid \forall x'.\forall y'.\ x'=e \land y'=y \rightarrow Q(x',y') \} \\ |
& = \{(x,y) \mid Q(e,y) \} = \{(x,y) \mid Q[x:=e]\} | & = \{(x,y) \mid Q(e,y) \} = \{(x,y) \mid Q[x:=e]\} | ||
\end{array} | \end{array} |