Who Cites mkgraphobj?
mkgraphobj	Def mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other) == < eq,eqw,eacc,eaccw,vacc,vaccw,other >
	Thm* For any graph eq:(VV), eqw:(x,y:V. eq(x,y) x = y), eacc:(T:Type. (TVT)TVT), eaccw:(T:Type, s:T, x:V, f:(TVT). L:V List. (y:V. x-the_graph- > y (y L)) & eacc(f,s,x) = list_accum(s',x'.f(s',x');s;L)), vacc:(T:Type. (TVT)TT), vaccw:(T:Type, s:T, f:(TVT). L:V List. no_repeats(V;L) & (y:V. (y L)) & vacc(f,s) = list_accum(s',x'.f(s',x');s;L)), other:Top. mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other) GraphObject(the_graph)

Syntax:

mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other)

has structure:

mkgraphobj(eq; eqw; eacc; eaccw; vacc; vaccw; other)

About: