p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y
x,y:V. x-the_graph- > *y 
Prop
PA:Prop. Dec(A) Propt:Graph. Vertices(t) Type
e:Type(e
vv)Top Type{i'}| Some definitions of interest. | |
| connect | Def x-the_graph- > *y == p:Vertices(the_graph) List. path(the_graph;p) & p[0] = x & last(p) = y |
| Thm* For any graph
x,y:V. x-the_graph- > *y Prop | |
| decidable | Def Dec(P) == P P |
| Thm* A:Prop. Dec(A) Prop | |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |