Nuprl - Proof: path-tl 1 2

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

At: path-tl 1 2

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

path(the_graph;tl(p))

By: MoveToConcl -1 THEN GenConcl (tl(p) = q)

Generated subgoals:

1 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) 2 steps

2 5. q: Vertices(the_graph) List
6. tl(p) = q
7. i: (||p||-1)
i < ||q|| 1 step

About:

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

1	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)`	2 steps

2	5. `q:` `Vertices(the_graph) List` 6. `tl(p) = q` 7. `i:` `(\|\|p\|\|-1)` `i < \|\|q\|\|`	1 step