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 01:12] mirco.dotta |
sav07_lecture_6 [2007/04/16 01:13] 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 185: | Line 186: | ||
[R]e<sub>T</sub> = {(a,s1(a)), (s1(a),s1(s1(a))), (s2(a), s2(s2(a))), ...} \\ | [R]e<sub>T</sub> = {(a,s1(a)), (s1(a),s1(s1(a))), (s2(a), s2(s2(a))), ...} \\ | ||
\\ | \\ | ||
- | Then we should find a pair (tx,ty) s.t. (tx,ty) ∉ [R]. A possible counter-example is (tx,a) ∉ [R], Vtx | + | Then we should find a pair (tx,ty) s.t. (tx,ty) ∉ [R]. A possible counter-example is (tx,a) ∉ [R], ∀tx |
\\ | \\ | ||
Consider case where R denotes less than relation on integers and Ev denotes that integer is even | Consider case where R denotes less than relation on integers and Ev denotes that integer is even |