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

At: connect transitivity 1
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
15. i: (||p1 @ tl(p)||-1)
(p1 @ tl(p))[i]-the_graph- > (p1 @ tl(p))[(i+1)]
By:
Analyze -6
THEN
All Reduce
THEN
Decide (i+1 < ||p1||)
Generated subgoals:

110. 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)]		1 step
 
210. 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)]		6 steps

About:
listnatural_numberaddsubtractless_thanequalall

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