2. to : {i:Id| T(i) }
(IdLnk List)
3. from : {i:Id| T(i) }
(IdLnk List)
4. u : IdLnk
5. i : |T|
6. (u
from(i))
7.
i:|T|.
7. (
lto(i).destination(l) = i
7. & T(source(l))
7. & (l
from(source(l)))
7. & (lnk-inv(l)
from(i)))
7. & (
lfrom(i).source(l) = i
7. & & T(destination(l))
7. & & (l
to(destination(l)))
7. & & (lnk-inv(l)
to(i)))
8. (
lto(i).destination(l) = i
8. & T(source(l))
8. & (l
from(source(l)))
8. & (lnk-inv(l)
from(i)))
9.
l:IdLnk.
9. (l
from(i))
9.
9. source(l) = i
9. & T(destination(l))
9. & (l
to(destination(l)))
9. & (lnk-inv(l)
to(i))
10. source(u) = i
11. T(destination(u))
12. (u
to(destination(u)))
13. (lnk-inv(u)
to(i))
T(source(u))
