(37steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: spanner-root-unique 1 2
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)
15. p:Edge(T) List. 0<||p||  lpath(p)  f(last(p))  (lp.f(l))
  i = j
By: DupHyp 5 THEN Unfold `bi-tree` -1 THEN ExRepD THEN InstHyp [i;j] -4 THEN ExRepD
THEN
Analyze -2
THEN
ExRepD

Generated subgoal:

1 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))  (lp.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. p : Edge(T) List
23. lpath(p)
24. ||p|| = 0    i = j  Id
25. ||p|| = 0    i = source(hd(p)) & j = destination(last(p))
26. q:Edge(T) List. lconnects(q;i;j)  q = p
  i = j
12 steps

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

(37steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc