Nuprl - Proof: path-tl 1 2 1

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

At: path-tl 1 2 1

1. the_graph: Graph
2. p: Vertices(the_graph) List
3. 1 < ||p||
4. path(the_graph;p)
5. q: Vertices(the_graph) List
6. tl(p) = q
7. ||q|| = ||p||-1
8. i:(||p||-1). q[i] = p[(i+1)]

path(the_graph;q)

By: All (Unfold `path`)

Generated subgoal:

1 4. 0 < ||p||
5. i:(||p||-1). p[i]-the_graph- > p[(i+1)]
6. q: Vertices(the_graph) List
7. tl(p) = q
8. ||q|| = ||p||-1
9. i:(||p||-1). q[i] = p[(i+1)]
10. i: (||q||-1)
q[i]-the_graph- > q[(i+1)] 1 step

About:

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