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

At: connect transitivity 1 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. u: Vertices(the_graph)
11. v: Vertices(the_graph) List
12. 0 < ||v||+1
13. i:(||v||+1-1). [u / v][i]-the_graph- > [u / v][(i+1)]
14. u = y
15. [u / v][(||v||+1-1)] = z
16. i: (||p1 @ v||-1)
17. i+1 < ||p1||
(p1 @ v)[i]-the_graph- > (p1 @ v)[(i+1)]
By: Decide (i = ||p1||-1)
Generated subgoals:

118. i = ||p1||-1
(p1 @ v)[i]-the_graph- > (p1 @ v)[(i+1)]		4 steps
 
218. i = ||p1||-1
(p1 @ v)[i]-the_graph- > (p1 @ v)[(i+1)]		1 step

About:
listconsintnatural_numberaddsubtractless_thanequalall

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