(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 1 2 1 1 2 1 2
1. T : Id
2. to : |T|(IdLnk List)
3. from : |T|(IdLnk List)
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)
11. ||p||||L||
12. n : ||p||
13. m : n
14. source(p[m]) = source(p[n])
15. p@0 : Edge(T) List
16. lconnects(p@0;source(p[m]);source(p[n]))
17. q:Edge(T) List. lconnects(q;source(p[m]);source(p[n]))  q = p@0
18. nil = p@0
19. lconnects(l_interval(p;m;n);source(p[m]);source(p[n]))
20. l_interval(p;m;n) = p@0
21. ||l_interval(p;m;n)|| = 0
  ||p||||L||
By: RWO Thm* l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j   -1

Generated subgoals:

None

About:
listnilboolintnatural_numberaddsubtractfunction
universeequalimpliesandallexists
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