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

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

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

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. p: Vertices(the_graph) List
7. p1:Vertices(the_graph) List. ||p1|| < ||p|| 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)
8. 0 < ||p||
9. i:(||p||-1). p[i]-the_graph- > p[(i+1)]
10. p[0] = x
11. last(p) = y
12. 1 < ||p||
13. p[1] = x
14. path(the_graph;tl(p))

p[1]-the_graph- > *y

By: Unfold `connect` 0 THEN InstConcl [tl(p)] THEN Try ((Unfold `path` -1) THEN ExRepD) THEN Try (RW assert_pushdownC 0) THEN Try (ObviousFrom [-2])

Generated subgoal:

1 14. 0 < ||tl(p)||
15. i:(||tl(p)||-1). tl(p)[i]-the_graph- > tl(p)[(i+1)]
last(tl(p)) = y 1 step

About:

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