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 ===== | ||