Nuprl - Proof: path-tl 1

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

At: path-tl 1

1. the_graph: Graph
2. p: Vertices(the_graph) List
3. 1 < ||p||
4. path(the_graph;p)

path(the_graph;tl(p))

By: Assert (||tl(p)|| = ||p||-1 & (i:(||p||-1). tl(p)[i] = p[(i+1)]))

Generated subgoals:

1 ||tl(p)|| = ||p||-1 & (i:(||p||-1). tl(p)[i] = p[(i+1)]) 3 steps

2 5. ||tl(p)|| = ||p||-1 & (i:(||p||-1). tl(p)[i] = p[(i+1)])
path(the_graph;tl(p)) 4 steps

About:

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

1	`\|\|tl(p)\|\| = \|\|p\|\|-1 & (i:(\|\|p\|\|-1). tl(p)[i] = p[(i+1)])`	3 steps

2	5. `\|\|tl(p)\|\| = \|\|p\|\|-1 & (i:(\|\|p\|\|-1). tl(p)[i] = p[(i+1)])` `path(the_graph;tl(p))`	4 steps