Nuprl - Some Definitions

	Some definitions of interest.

graphrep	`Def Graph Representation == type:Typegraph:typeGraphr:typeGraphObject(graph(r))`

	`Thm* Graph Representation Type{i'}`

graphobj	Def GraphObject(the_graph) == eq:Vertices(the_graph)Vertices(the_graph)(x,y:Vertices(the_graph). (eq(x,y)) x = y)(eacc:(T:Type. (TVertices(the_graph)T)TVertices(the_graph)T)(T:Type, s:T, x:Vertices(the_graph), f:(TVertices(the_graph)T). L:Vertices(the_graph) List. (y:Vertices(the_graph). x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L))(vacc:(T:Type. (TVertices(the_graph)T)TT)(T:Type, s:T, f:(TVertices(the_graph)T). L:Vertices(the_graph) List. no_repeats(Vertices(the_graph);L) & (y:Vertices(the_graph). (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L))Top))

	`Thm* the_graph:Graph. GraphObject(the_graph) Type{i'}`

grr_graph	`Def t.graph == 1of(2of(t))`

	`Thm* t:Graph Representation. t.graph t.typeGraph`

grr_obj	`Def t.obj == 2of(2of(t))`

	`Thm* t:Graph Representation. t.obj r:t.typeGraphObject(t.graph(r))`

grr_type	`Def t.type == 1of(t)`

	`Thm* t:Graph Representation. t.type Type`

About: