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:atomic_diagram_normal_form [2009/05/12 22:59] vkuncak |
sav08:atomic_diagram_normal_form [2009/05/12 23:24] vkuncak |
||
|---|---|---|---|
| Line 2: | Line 2: | ||
| We next consider a syntactic normal form that helps us understand the decidability of the combination problem. | We next consider a syntactic normal form that helps us understand the decidability of the combination problem. | ||
| + | |||
| ===== Flat Form ===== | ===== Flat Form ===== | ||
| Line 20: | Line 21: | ||
| \[ | \[ | ||
| C[t] \ \ \leadsto \ \ (x=t) \land C[x] | C[t] \ \ \leadsto \ \ (x=t) \land C[x] | ||
| + | \] | ||
| + | |||
| + | **Example:** Represent $f(x)+y < z$ as | ||
| + | \[ | ||
| + | x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z | ||
| \] | \] | ||