Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:compositional_vcg [2009/03/04 23:49] vkuncak |
sav08:compositional_vcg [2009/03/04 23:50] vkuncak |
||
---|---|---|---|
Line 32: | Line 32: | ||
\forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) | \forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) | ||
\] | \] | ||
+ | |||
Line 79: | Line 80: | ||
F_c(c_1\ ;\ c_2)\ =\ (\exists \vec z. F_c(c_1)[\vec x':=\vec z] \land F_c(c_2)[\vec x:=\vec z]) | F_c(c_1\ ;\ c_2)\ =\ (\exists \vec z. F_c(c_1)[\vec x':=\vec z] \land F_c(c_2)[\vec x:=\vec z]) | ||
\] | \] | ||
- | To avoid re-using variables, introduce always a fresh variable as //\vec z//, denote it $\vec z_i$. | + | Above, $F_c(c_1)[\vec x':=\vec z]$ denotes taking formula $F_c(c_1)$ and replacing in it occurrences of variables $\vec x'$ by variables $\vec z$. |
+ | |||
+ | To avoid re-using variables, introduce always a fresh variable as $\vec z$ and denote it $\vec z_i$. | ||
===== Using Computed Formulas ===== | ===== Using Computed Formulas ===== |