(31steps 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: bi-tree-diameter 1
1. T : Id
2. to : |T|(IdLnk List)
3. from : |T|(IdLnk List)
4. bi-tree(T;to;from)
  n:. p:Edge(T) List. lpath(p)  ||p||n
By: Analyze -1 THEN ExRepD THEN InstConcl [||L||]

Generated subgoals:

1 4. bi-graph(T;to;from)
5. i,j:|T|.
5. p:Edge(T) List. 
5. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
6. L : |T| List
7. i:|T|. (i  L)
8. |T|
9. p : Edge(T) List
10. lpath(p)
  ||p||||L||
27 steps
2 4. bi-graph(T;to;from)
5. i,j:|T|.
5. p:Edge(T) List. 
5. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
6. L : |T| List
7. i:|T|. (i  L)
8. |T|
9. Edge(T) List
10. Edge(T) List
11. u : Edge(T)
  u  IdLnk
1 step
3 4. bi-graph(T;to;from)
5. i,j:|T|.
5. p:Edge(T) List. 
5. lconnects(p;i;j) & (q:Edge(T) List. lconnects(q;i;j)  q = p)
6. L : |T| List
7. i:|T|. (i  L)
8. |T|
9. 
10. Edge(T) List
11. Edge(T) List
12. u : Edge(T)
  u  IdLnk
1 step

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

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