1. G : Id
2. to : |G|(IdLnk List)
3. from : |G|(IdLnk List)
4. e : Edge(G)
5. bi-graph(G;to;from)
  Dec((e  to(destination(e))))

1	6. x : Edge(G) 7. y : Edge(G)   Dec(x = y)	1 step
2	destination(e)  |G|	1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html