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

At: connect transitivity 2 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. 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. 1 < ||p||
tl(p)[(||p1||+||tl(p)||-1-||p1||)] = z
By: RWO Thm* as:A List, n:(||as||-1). tl(as)[n] = as[(n+1)] 0
Generated subgoals:

1 ||p1||+||tl(p)||-1-||p1|| (||p||-1)1 step
 
2 p[(||p1||+||tl(p)||-1-||p1||+1)] = z2 steps

About:
listnatural_numberaddsubtractless_thanuniverseequalmemberall

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