IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
spanner-root-unique
1
2
1
2
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. L1 : |T| List
9.
i:|T|. (i
L1)
10. |T|
11. spanner(f;T;to;from)
12. i : |T|
13. j : |T|
14. spanner-root(f;T;to;from;i)
15. spanner-root(f;T;to;from;j)
16.
p:Edge(T) List. 0<||p|| 
lpath(p) 
f(last(p)) 
(
l
p.f(l))
17. bi-graph(T;to;from)
18.
i,j:|T|.
18.
p:Edge(T) List.
18. lconnects(p;i;j) & (
q:Edge(T) List. lconnects(q;i;j) 
q = p)
19. L : |T| List
20.
i:|T|. (i
L)
21. |T|
22. u : Edge(T)
23. v : Edge(T) List
24. lpath([u / v])
25. ||v||+1 = 0 
i = j
26.
||v||+1 = 0 
i = source(u) & j = destination(last([u / v]))
27.
q:Edge(T) List. lconnects(q;i;j) 
q = [u / v]
(
l
[u / v].f(l))
Generated subgoal:
| 1 |
f(last([u / v]))
 | 3 steps |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html