Nuprl - graph_1_3 Citations of adjm-edge-accum

Def adjm-edge-accum(M;s',x'.f(s';x');s;x) == primrec(M.size;s;

y,s'. if M.adj(x,y)

f(s';y) else s' fi)

is mentioned by

Thm* M:AdjMatrix, T:Type, s:T, x:Vertices(adjm-graph(M)), f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. (y:Vertices(adjm-graph(M)). x-adjm-graph(M)- > y (y L)) & adjm-edge-accum(M;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L) [adjm-edge-accum-properties]

Def adjm-obj{\\\\v:l,i:l}(M) == mkgraphobj(x,y. x =M= y, ext{assert_eq_adjm}(M), f,s,x. adjm-edge-accum(M;s',x'.f(s',x');s;x), ext{adjm_DASH_edge_DASH_accum_DASH_properties}{i:l}(M), f,s. adjm-vertex-accum(M;s',x'.f(s',x');s), ext{adjm_DASH_vertex_DASH_accum_DASH_properties}{i:l}(M), ) [adjm-obj]

Try larger context: Graphs

graph 1 3 Sections Graphs Doc

`Thm* M:AdjMatrix, T:Type, s:T, x:Vertices(adjm-graph(M)), f:(TVertices(adjm-graph(M))T). L:Vertices(adjm-graph(M)) List. (y:Vertices(adjm-graph(M)). x-adjm-graph(M)- > y (y L)) & adjm-edge-accum(M;s',x'.f(s',x');s;x) = list_accum(s',x'.f(s',x');s;L)`	[adjm-edge-accum-properties]
`Def adjm-obj{\\\\v:l,i:l}(M) == mkgraphobj(x,y. x =M= y, ext{assert_eq_adjm}(M), f,s,x. adjm-edge-accum(M;s',x'.f(s',x');s;x), ext{adjm_DASH_edge_DASH_accum_DASH_properties}{i:l}(M), f,s. adjm-vertex-accum(M;s',x'.f(s',x');s), ext{adjm_DASH_vertex_DASH_accum_DASH_properties}{i:l}(M), )`	[adjm-obj]