(9steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc

At: path-tl 1 1 2
1. the_graph: Graph
2. p: Vertices(the_graph) List
3. 1 < ||p||
4. path(the_graph;p)
5. i: (||p||-1)
tl(p)[i] = p[(i+1)]
By: RWO Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] 0
Generated subgoals:

None

About:
listnatural_numberaddsubtractless_thanuniverseequalall

(9steps total) PrintForm Definitions Lemmas graph 1 2 Sections Graphs Doc