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. u : Edge(T)
18. v : Edge(T) List
19. lpath([u / v])
20. ||[u / v]|| = n-1
21. (l[u / v].f(l))
  p:Edge(T) List. lpath(p) & ||p|| = n   & (lp.f(l))

By:

RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) -1 THEN AssertBY (lto(source(u)).f(l)) (BackThruSomeHyp (THEN (BackThru (Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T). (Thm* bi-graph(T;to;from)  source(u)  |T|) THEN Analyze -1 THEN InstConcl [[l; u / v]] THEN All Reduce THEN MaAuto

1	20. ||v||+1 = n-1 21. f(u) 22. (lv.f(l)) 23. l : Edge(T) 24. (l  to(source(u))) 25. f(l)   lpath([l; u / v])	11 steps
2	20. ||v||+1 = n-1 21. f(u) 22. (lv.f(l)) 23. l : Edge(T) 24. (l  to(source(u))) 25. f(l)   (l[l; u / v].f(l))	1 step

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