Nuprl - Some Definitions

	Some definitions of interest.

df-traversal	`Def df-traversal(G;s) == (i:Vertices(G), s1,s2:traversal(G). s = (s1 @ [inr(i)] @ s2) traversal(G) (j:Vertices(G). (inr(j) s2) (inl(j) s2) j-G- > i)) & (i:Vertices(G), s1,s2:traversal(G). (j:Vertices(G). i-G- > j non-trivial-loop(G;j)) s = (s1 @ [inl(i)] @ s2) traversal(G) (j:Vertices(G). i-G- > *j (inr(j) s2)))`

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

About: