x,y:V. Dec(x = y)) 
(x,y:V. x-the_graph- > *y 
x = y 
(
z:V. 
z = x & x-the_graph- > z & z-the_graph- > *y))x,y:V. x-the_graph- > y x-the_graph- > *yi:
(||p||-1). p[i]-the_graph- > p[(i+1)])e:Edges(the_graph). Incidence(the_graph)(e) = < x,y >
is mentioned by
| Thm* For any graph
(x,y:V. Dec(x = y)) (x,y:V. x-the_graph- > *y x = y (z:V. z = x & x-the_graph- > z & z-the_graph- > *y)) | [connect-iff] |
| Thm* For any graph
x,y:V. x-the_graph- > y x-the_graph- > *y | [edge-connect] |
| Def path(the_graph;p) == 0 < ||p|| & (i:(||p||-1). p[i]-the_graph- > p[(i+1)]) | [path] |
Try larger context:
Graphs