Who Cites vertex-count?
vertex-count	Def vertex-count(the_obj;x.P(x)) == ||vertex-subset(the_obj;x.P(x))||
vertex-subset	Def vertex-subset(the_obj;x.P(x)) == the_obj.vacc((l,x. if P(x) [x / l] else l fi),nil)
length	Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
	Thm* A:Type, l:A List. ||l||
	Thm* ||nil||
gro_vacc	Def t.vacc == 1of(2of(2of(2of(2of(t)))))
	Thm* For any graph t:GraphObject(the_graph), T:Type. t.vacc (TVT)TT
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:

vertex-count(the_obj;x.P(x))

has structure:

vertex-count(the_obj; x.P(x))

About: