T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
  bi-graph(T;to;from)  destination(u)  |T|

1

1. T : Id 2. to : {i:Id| T(i) }(IdLnk List) 3. from : {i:Id| T(i) }(IdLnk List) 4. u : {l:IdLnk| i:|T|. (l  from(i)) } 5. i:|T|.  5. (lto(i).destination(l) = i 5. & T(source(l)) 5. & (l  from(source(l))) 5. & (lnk-inv(l)  from(i))) 5. & (lfrom(i).source(l) = i 5. & & T(destination(l)) 5. & & (l  to(destination(l))) 5. & & (lnk-inv(l)  to(i)))   T(destination(u))

1 step

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html