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

At: path-tl 1 1
1. the_graph: Graph
2. p: Vertices(the_graph) List
3. 1 < ||p||
4. path(the_graph;p)
||tl(p)|| = ||p||-1 & (i:(||p||-1). tl(p)[i] = p[(i+1)])
By: Auto
Generated subgoals:

1 ||tl(p)|| = ||p||-1 1 step
 
25. i: (||p||-1)
tl(p)[i] = p[(i+1)]		1 step

About:
listintnatural_numberaddsubtractless_thanequalandall

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