p:V List. 1 < ||p|| 
path(the_graph;p) path(the_graph;tl(p))
p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = yi:
(||p||-1). p[i]-the_graph- > p[(i+1)])
is mentioned by
| Thm* For any graph
p:V List. 1 < ||p|| path(the_graph;p) path(the_graph;tl(p)) | [path-tl] |
| Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y | [connect] |
Try larger context:
Graphs