Nuprl - Some Definitions

	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`

edge	`Def x-the_graph- > y == e:Edges(the_graph). Incidence(the_graph)(e) = < x,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'}`

not	`Def A == A False`

	`Thm* A:Prop. (A) Prop`

About: