Nuprl - graph_1_3 LEMMAs for adjl_DASH_vertex_DASH_accum_DASH

Rank	Theorem	Name
4	Thm* A:AdjList, T:Type, s:T, f:(TVertices(adjl-graph(A))T). L:Vertices(adjl-graph(A)) List. no_repeats(Vertices(adjl-graph(A));L) & (y:Vertices(adjl-graph(A)). (y L)) & adjl-vertex-accum(A;s',x'.f(s',x');s) = list_accum(s',x'.f(s',x');s;L)	[adjl-vertex-accum-properties]
cites
3	Thm* i,j:. no_repeats(;upto(i;j))	[no_repeats_upto]
2	Thm* i,j,k:. (k upto(i;j)) ik & k < j	[member_upto]
0	Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))	[primrec_list_accum]