1. T : Id
2. to : |T|(IdLnk List)
3. from : |T|(IdLnk List)
4. f : Edge(T)
5. bi-graph(T;to;from)
6. i,j:|T|.
6. p:Edge(T) List. 
6. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
7. L : |T| List
8. i:|T|. (i  L)
9. j : |T|
10. bi-graph(T;to;from)
11. spanner(f;T;to;from)
12. ||to(j)|| = 0
13. (i:|T|. l:Edge(T). (l  to(i))  f(l))
14. i:|T|. (lto(i).f(l))
15. n : 
16. 0<n
17. lpath(nil)
18. ||nil|| = n-1
19. (lnil.f(l))
20. l : Edge(T)
21. (l  to(j))
22. f(l)
  (l[l].f(l))

By:	RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) 0

None

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