Nuprl - Some Definitions

	Some definitions of interest.

list-connect	`Def L-G- > x == (yL.y-G- > x)`

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`

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'}`

l_member	`Def (x l) == i:. i < \|\|l\|\| & x = l[i] T`

	`Thm* T:Type, x:T, l:T List. (x l) Prop`

About: