Nuprl - Proof: bi-tree-diameter 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: bi-tree-diameter 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. Edge(T) List
10. Edge(T) List
11. u : Edge(T)

IdLnk

By:

MaAuto

Generated subgoals:

None

About:

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