T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)).
  bi-tree(T;to;from)
  
  spanner(f;T;to;from)
  
  (i,j:|T|.
  (spanner-root(f;T;to;from;i)  spanner-root(f;T;to;from;j)  i = j)

1

1. T : Id 2. to : |T|(IdLnk List) 3. from : |T|(IdLnk List) 4. f : Edge(T) 5. bi-tree(T;to;from) 6. bi-graph(T;to;from) 7. i,j:|T|. 7. p:Edge(T) List.  7. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p) 8. L:|T| List. i:|T|. (i  L) 9. |T| 10. spanner(f;T;to;from) 11. i : |T| 12. j : |T| 13. spanner-root(f;T;to;from;i) 14. spanner-root(f;T;to;from;j)   i = j

36 steps

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