Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_6 [2007/04/16 00:05] mirco.dotta |
sav07_lecture_6 [2007/04/16 00:08] mirco.dotta |
||
|---|---|---|---|
| Line 125: | Line 125: | ||
| \end{equation*} | \end{equation*} | ||
| where $\theta$ is the most general unifier of $A_1$ and $A_2$. | where $\theta$ is the most general unifier of $A_1$ and $A_2$. | ||
| + | |||
| Line 168: | Line 169: | ||
| by: Adding a constant 'a' | by: Adding a constant 'a' | ||
| R.{s1,s2,a} = L \\ | R.{s1,s2,a} = L \\ | ||
| + | \\ | ||
| + | Term(L) = {a, s1(a), s2(a), s1(s1(a)), ...} \\ | ||
| \\ | \\ | ||
| [R]e<sub>T</sub> = {(t,s1(t)) | t ∈ Term(L)} where e<sub>T</sub>: F => {true, false} and T => Term(L)\\ | [R]e<sub>T</sub> = {(t,s1(t)) | t ∈ Term(L)} where e<sub>T</sub>: F => {true, false} and T => Term(L)\\ | ||