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

At: connect transitivity 2
1. the_graph: Graph
2. x: Vertices(the_graph)
3. y: Vertices(the_graph)
4. z: Vertices(the_graph)
5. p1: Vertices(the_graph) List
6. 0 < ||p1||
7. i:(||p1||-1). p1[i]-the_graph- > p1[(i+1)]
8. p1[0] = x
9. p1[(||p1||-1)] = y
10. p: Vertices(the_graph) List
11. 0 < ||p||
12. i:(||p||-1). p[i]-the_graph- > p[(i+1)]
13. p[0] = y
14. p[(||p||-1)] = z
(p1 @ tl(p))[(||p1 @ tl(p)||-1)] = z
By: Decide (1 < ||p||)
Generated subgoals:

115. 1 < ||p||
(p1 @ tl(p))[(||p1 @ tl(p)||-1)] = z		6 steps
 
215. 1 < ||p||
(p1 @ tl(p))[(||p1 @ tl(p)||-1)] = z		5 steps

About:
listnatural_numberaddsubtractless_thanequalall

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