Nuprl - Some Definitions

	Some definitions of interest.

depthfirst	`Def depthfirst(the_obj) == the_obj.vacc((s,i. dfs(the_obj;s;i)),nil)`

	`Thm* For any graph the_obj:GraphObject(the_graph). depthfirst(the_obj) Traversal`

dfs	`Def dfs(the_obj;s;i) == if member-paren(x,y.the_obj.eq(x,y);i;s) s else [inl(i) / (the_obj.eacc((s',j. dfs(the_obj;s';j)),[inr(i) / s],i))] fi (recursive)`

	`Thm* For any graph the_obj:GraphObject(the_graph), s:Traversal, i:V. dfs(the_obj;s;i) Traversal`

graph	`Def Graph == v:Typee:Type(evv)Top`

	`Thm* Graph 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'}`

gro_vacc	`Def t.vacc == 1of(2of(2of(2of(2of(t)))))`

	`Thm* For any graph t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT`

traversal	`Def traversal(G) == (Vertices(G)+Vertices(G)) List`

	`Thm* For any graph Traversal Type`

About: