tree_paths[T: TYPE]: THEORY
BEGIN
IMPORTING tree_circ[T], paths[T]
GT: VAR Tree
u,v: VAR T
m,n: VAR nat
G: VAR graph[T]
tree_path_reduced: LEMMA FORALL (w1,w2: prewalk): % **** NOT YET PROVED
path_from?(GT, w1, u, v) AND
path_from?(GT, w2, u, v) AND
l(w1) > 1 AND w1 /= w2 AND
pre_circuit?(GT, w1 ^ (0, l(w1) - 2) o rev(w2))
IMPLIES cyclically_reduced?(GT, w1 ^ (0, l(w1) - 2) o rev(w2))
w1,w2: VAR prewalk
tree_one_path: LEMMA FORALL (w1,w2: prewalk): tree?(GT) AND % ** NOT YET PROVED
path_from?(GT,w1,u,v) AND
path_from?(GT,w2,u,v) IMPLIES
w1 = w2
END tree_paths