1. G : Id
2. to : |G|(IdLnk List)
3. from : |G|(IdLnk List)
4. e : Edge(G)
5. i : |G|
6. bi-graph(G;to;from)
7. (e  to(i))
8. i:|G|. 
8. (lto(i).destination(l) = i
8. & G(source(l))
8. & (l  from(source(l)))
8. & (lnk-inv(l)  from(i)))
8. & (lfrom(i).source(l) = i
8. & & G(destination(l))
8. & & (l  to(destination(l)))
8. & & (lnk-inv(l)  to(i)))
9. l:IdLnk. 
9. (l  to(i))
9. 
9. destination(l) = i
9. & G(source(l))
9. & (l  from(source(l)))
9. & (lnk-inv(l)  from(i))
10. (lfrom(i).source(l) = i
10. & G(destination(l))
10. & (l  to(destination(l)))
10. & (lnk-inv(l)  to(i)))
  (e  to(i))

By:	Using [`A',Edge(G)] (BackThru Thm* L:A List, x:A. (A r B)  (x  L)  (x  L)) THEN MaAuto THEN Analyze 0 THEN MaAuto

None

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