Nuprl - Some Definitions

	Some definitions of interest.

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

append	`Def as @ bs == Case of as; nil bs ; a.as' [a / (as' @ bs)] (recursive)`

	`Thm* T:Type, as,bs:T List. (as @ bs) T List`

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

non-trivial-loop	`Def non-trivial-loop(G;i) == j:Vertices(G). j = i & i-G- > j & j-G- > i`

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`

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

	`Thm* For any graph Traversal Type`

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`

not	`Def A == A False`

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

About: