2. to : |G|
(IdLnk List)
3. from : |G|
(IdLnk List)
4. e : IdLnk
5. i : |G|
6. (e
from(i))
7. bi-graph(G;to;from)
8. e
Edge(G)
9.
i:|G|.
9. (
lto(i).destination(l) = i
9. & G(source(l))
9. & (l
from(source(l)))
9. & (lnk-inv(l)
from(i)))
9. & (
lfrom(i).source(l) = i
9. & & G(destination(l))
9. & & (l
to(destination(l)))
9. & & (lnk-inv(l)
to(i)))
10. (
lto(i).destination(l) = i
10. & G(source(l))
10. & (l
from(source(l)))
10. & (lnk-inv(l)
from(i)))
11.
l:IdLnk.
11. (l
from(i))
11.
11. source(l) = i
11. & G(destination(l))
11. & (l
to(destination(l)))
11. & (lnk-inv(l)
to(i))
12. source(e) = i
13. G(destination(e))
14. i1 :
15. e = (to(destination(e)))[i1]
e = (to(destination(e)))[i1] Edge(G)
