(35steps 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-exists 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. spanner(f;T;to;from)
  i:|T|. spanner-root(f;T;to;from;i)
By: FwdThru
Thm* T:(Id), to,from:(|T|(IdLnk List)).
Thm* bi-tree(T;to;from)  (n:. p:Edge(T) List. lpath(p)  ||p||n)
[-3]
THEN
Unfold `bi-tree` 5
THEN
ExRepD
THEN
RenameVar `j' 9
THEN
Decide (||to(j)|| = 0)

Generated subgoals:

1 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. n : 
13. p:Edge(T) List. lpath(p)  ||p||n
14. ||to(j)|| = 0  
  i:|T|. spanner-root(f;T;to;from;i)
1 step
2 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. n : 
13. p:Edge(T) List. lpath(p)  ||p||n
14. ||to(j)|| = 0  
  i:|T|. spanner-root(f;T;to;from;i)
32 steps

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

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