# RE: [PVS-Help] Trees and prewalks

```I would go with

[1] tree_path: LEMMA
FORALL (G: Tree, i: T, j: T | i /= j):
vert(G)(i) AND vert(G)(j) IMPLIES
EXISTS (pw: walk): path_from?(G, pw, i, j)

You need an existential quantifier.  I would make it a walk not a
prewalk.
A prewalk is just a sequence of vertices, but they need not have an edge
between them.

Rick

-----Original Message-----
From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
[mailto:pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf
Of Jerome
Sent: Friday, November 14, 2008 7:20 PM
To: PVS Help
Subject: [PVS-Help] Trees and prewalks

I would like to prove that all points within a non-singleton tree are
"reachable."  That is, from a given point you can reach any other point
in the tree. I'm wondering which of the following is the proper way to
pose the lemma in PVS:

[1] tree_path: LEMMA
FORALL (G: Tree, i: T, j: T | i /= j):
vert(G)(i) AND vert(G)(j) IMPLIES
FORALL (pw: prewalk): path_from?(G, pw, i, j)

or

[2] tree_path: LEMMA
FORALL (G: Tree, i: T, j: T | i /= j):
vert(G)(i) AND vert(G)(j) IMPLIES
FORALL (pw: Path(G)): path_from?(G, pw, i, j)

Thanks

jerome

```