Answer to question 1:  See
    Paige and Koenig, "Finite Differencing of Computable Expressions,"
    TOPLAS, Vol. 4, No. 3, 1982.

a.  (proof sketch) Prove that the first specification is well defined.
That is, prove that the construction yields a longest path in T, and
that the sets of middle elements of every longest path in T must be
the same.  Hence, it suffices to find the middle vertices of any
longest path.  Next prove that the tree center algorithm in cent.stl
computes the middle elements of some one longest path.

proof sketch that the construction yields a longest path)
1.  If y is furthest from an arbitrary vertex x, then every longest path
in T must include a vertex on line x-y.  (proof by contradiction)
2.  Vertex y must be included in some longest path.  (follows from 1.
and by contradiction)

proof sketch that the middle elements of every longest path in T must be the
same)
3.  Any two longest paths in T must intersect.  (follows from 1.)
4.  The middle vertices of any two longest paths is the same.  (follows
from 3. and by contradiction)

proof sketch that the tree center algorithm in cent.stl computes the middle
elements of some one longest path.  (by induction on the length of such a
path)

b.  The SETL2 specification of the tree center problem is based on the
following ideas:

Input a set e of edges, where each edge is a set of two distinct vertices.
Assume that e is a free tree.  Then the following definitions may be useful:

1.  The nodes of any subset s of edges,

nodes(s) = +/s

2.  The edges in s incident to a given node x,

neighbors(x,s) = {y in s | x in y}

3.  The leaf nodes of s

leaves(s) = {x in nodes(s) | #neighbors(x,s) = 1}

4.  All vertices reachable along paths in e reachable from vertex x.

See reach.stl

5.  Decision whether a set s of edges is connected,

connected(s) <-> forall x in nodes(s) | reach(x) = s

6.  Decision whether a set of edges s in a free tree e forms a path,

path(s) <-> connected(s) and (#leaves(s)=2 and 
              forall x in (nodes(s) - leaves(s)) | #neighbors(x,s) = 2)

7.  All paths in e from a node x,

paths(x) = {s in pow(e) | path(s) and x in leaves(s)}

8.  All longest paths in e from a node x,

maxpaths(x) = {s in paths(x) | #s = max/{#q: q in paths(x)}}

9.  All nodes furthest from a given node x,

furthest(x) = {y: s in maxpaths(x), y in leaves(s) | y /= x}

10.  A maximal path obtained by Archisman Rudra's construction

arb maxpaths( arb furthest(arb nodes(e)))

11.  The middle of a longest path s contained in a free tree

middle(s) = {x in nodes(s) | #(arb maxpaths(x)) = #s/2 + #s mod 2}

where #s/2 + #s mod 2 = ceiling(real(#s)/2.))

12.  Tree Center

middle(arb maxpaths( arb furthest(arb nodes(e)))