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

At: path-tl 1 1 1
1. the_graph: Graph
2. p: Vertices(the_graph) List
3. 1 < ||p||
4. path(the_graph;p)
||tl(p)|| = ||p||-1
By: RWO Thm* l:A List. ||l||1 ||tl(l)|| = ||l||-1 0
Generated subgoals:

None

About:
listintnatural_numbersubtractless_thanuniverseequalimpliesall

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