RE: [PVS-Help] Trees and prewalks

["Butler, Ricky W. (LARC-D320)" <R.W.Butler@xxxxxxxx>]

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