[PVS-Help] Trees and prewalks

[Jerome <jerome@xxxxxxxxxxxxxx>]

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