Nuprl - Proof: connect-iff 1 1 1 1 2 1 1 3 1

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

At: connect-iff 1 1 1 1 2 1 1 3 1

1. the_graph: Graph
2. x,y:Vertices(the_graph). Dec(x = y)
3. x: Vertices(the_graph)
4. y: Vertices(the_graph)
5. n:
6. u: Vertices(the_graph)
7. v: Vertices(the_graph) List
8. p1:Vertices(the_graph) List. ||p1|| < ||v||+1 path(the_graph;p1) p1[0] = x last(p1) = y x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > *y)
9. path(the_graph;[u / v])
10. [u / v][0] = x
11. last([u / v]) = y
12. 1 < ||v||+1
13. [u / v][1] = x
14. path(the_graph;v)

last(v) = y

By: RWO Thm* L:T List, x:T. null(L) last([x / L]) = last(L) -4

Generated subgoal:

1 null(v) 1 step

About:

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