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

At: connect-iff 1 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. p: Vertices(the_graph) List
6. path(the_graph;p)
7. p[0] = x
8. last(p) = y
x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > *y)
By:
RepeatFor 4 (MoveToConcl -1)
THEN
InductionOnLength
Generated subgoals:

15. 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. path(the_graph;p)
9. p[0] = x
10. last(p) = y
x = y (z:Vertices(the_graph). z = x & x-the_graph- > z & z-the_graph- > *y)		18 steps
 
25. 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. path(the_graph;p)
9. p[0] = x
null(p)		3 steps
 
35. 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. path(the_graph;p)
0 < ||p||		1 step

About:
listassertdecidablenatural_numberless_thanequalandorallexists

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