(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 1 1 1 1 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. i:|T|i@0:i@0<||L|| & i = L[i@0]
13. (n:||p||, m:n. source(p[m]) = source(p[n]))
14. a1 : ||p||
15. a2 : ||p||
16. source(p[a1]) = source(p[a2])
17. a1a2
  a1 = a2
By: Analyze -5 THEN InstConcl [a1;a2]
THEN
Try
(BackThru
(Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
(Thm* bi-graph(T;to;from)  source(u)  |T|)

Generated subgoals:

None

About:
productlistboolnatural_numberless_thanfunction
equalmemberimpliesandallexists
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