Def		t.eqw	[gro_eqw]
Def		t.eaccw	[gro_eaccw]
Def		t.vaccw	[gro_vaccw]
Def		t.other	[gro_other]
Def		For any graph representation P(the_graph;the_obj)	[allgrep]
Def		adjm-rep{\\\\v:l,i:l}()	[adjm-rep]
Def		AdjListRep	[adjl-rep]
Def		adjl_to_adjm(l)	[adjl_to_adjm]
Def		vertex-count(the_obj;x.P(x))	[vertex-count]
Def		l_disjoint(T;l1;l2)	[l_disjoint]	mb list 2
Def		dfsl-traversal(the_graph;L;s)	[dfsl-traversal]	graph 1 2
Def		df-traversal(G;s)	[df-traversal]	graph 1 2
Def		depthfirst-traversal(the_graph;s)	[depthfirst-traversal]	graph 1 2
Def		topsorted(the_graph;s)	[topsorted]	graph 1 2
Def		non-trivial-loop-free(G)	[non-trivial-loop-free]	graph 1 2
Def		dfl-traversal(the_graph;L;s)	[dfl-traversal]	graph 1 2
Def		topsortedl(the_graph;L;s)	[topsortedl]	graph 1 2
Def		non-trivial-loop(G;i)	[non-trivial-loop]	graph 1 2
Def		L-G- > *x	[list-connect]	graph 1 2
Def		x-the_graph- > *y	[connect]	graph 1 2
Def		(xL.P(x))	[l_all]	mb list 2
Def		Graph Representation	[graphrep]
Def		GraphObject(the_graph)	[graphobj]
Def		no_repeats(T;l)	[no_repeats]	mb list 2
Def		(xL.P(x))	[l_exists]	mb list 2
Def		(x l)	[l_member]	mb list 1
Def		adjm-graph(A)	[adjm-graph]
Def		AdjMatrix	[adjmatrix]
Def		adjl-graph(G)	[adjl-graph]
Def		AdjList	[adjlist]
Def		path(the_graph;p)	[path]	graph 1 2
Def		x before y l	[l_before]	mb list 1
Def		L1 L2	[sublist]	mb list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def			[nat]	int 1
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P Q	[implies]	core
Def		Dec(P)	[decidable]	core
Def		A	[not]	core
Def		traversal(G)	[traversal]	graph 1 2
Def		paren(T;s)	[paren]	graph 1 2
Def		as @ bs	[append]	list 1
Def		Prop	[prop]	core
Def		P Q	[or]	core
Def		topsort(G)	[topsort]
Def		topsortl(A;L)	[topsortl]
Def		adjm_to_adjl(m)	[adjm_to_adjl]
Def		G H	[graph-isomorphic]	graph 1 2
Def		Graph	[graph]	graph 1 2
Def		Top	[top]	core
Def		dfsl(G;L)	[dfsl]
Def		adjl-obj{\\\\v:l,i:l}(A)	[adjl-obj]
Def		adjl-edge-accum(A;s',x'.f(s';x');s;x)	[adjl-edge-accum]
Def		list_accum(x,a.f(x;a);y;l)	[list_accum]	mb list 1
Def		x-the_graph- > y	[edge]	graph 1 2
Def		P & Q	[and]	core
Def		x:A. B(x)	[exists]	core
Def		b	[assert]	bool 1
Def		P Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def			[bool]	bool 1
Def		Vertices(t)	[gr_v]	graph 1 2
Def		vertex-subset(the_obj;x.P(x))	[vertex-subset]
Def		depthfirst(the_obj)	[depthfirst]
Def		t.vacc	[gro_vacc]
Def		t.graph	[grr_graph]
Def		t.type	[grr_type]
Def		dfs(the_obj;s;i)	[dfs]
Def		t.eacc	[gro_eacc]
Def		t.eq	[gro_eq]
Def		adjm-obj{\\\\v:l,i:l}(M)	[adjm-obj]
Def		adjm-vertex-accum(M;s',x.f(s';x);s)	[adjm-vertex-accum]
Def		adjm-edge-accum(M;s',x'.f(s';x');s;x)	[adjm-edge-accum]
Def		t.size	[adjm_size]
Def		adjl-vertex-accum(A;s',x.f(s';x);s)	[adjl-vertex-accum]
Def		t.size	[adjl_size]
Def		Incidence(t)	[gr_f]	graph 1 2
Def		Edges(t)	[gr_e]	graph 1 2
Def		1of(t)	[pi1]	core
Def		t.obj	[grr_obj]
Def		t.adj	[adjm_adj]
Def		t.out	[adjl_out]
Def		2of(t)	[pi2]	core
Def		if b t else f fi	[ifthenelse]	bool 1
Def		last(L)	[last]	mb list 1
Def		||as||	[length]	list 1
Def		member-paren(x,y.E(x;y);i;s)	[member-paren]	graph 1 2
Def		Y	[ycomb]	core
Def		mapoutl(s)	[mapoutl]	graph 1 1
Def			[it]	core
Def		< vertices = v, edges = e, incidence = f >	[mkgraph]	graph 1 2
Def		primrec(n;b;c)	[primrec]	mb nat
Def		x =M= y	[eq_adjm]
Def		x =A= y	[eq_adjl]
Def		i=j	[eq_int]	bool 1
Def		mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other)	[mkgraphobj]
Def		mkgraphrep(type, graph, obj)	[mkgraphrep]
Def		l[i]	[select]	list 1
Def		upto(i;j)	[upto]	graph 1 1
Def		mapfilter(f;P;L)	[mapfilter]	mb list 2
Def		filter(P;l)	[filter]	mb list 1
Def		mk_adjlist(size, out)	[mk_adjlist]
Def		Case mk_adjmatrix(size,adj) = > body(size;adj)	[case_mk_adjmatrix]
Def		Case(value) body	[case]	prog 1
Def		(xL.P(x))	[l_bexists]	graph 1 1
Def		mk_adjmatrix(size, adj)	[mk_adjmatrix]
Def		Case mk_adjlist(size; out ) = > body(size;out)	[case_mk_adjlist]
Def		f o g	[compose]	fun 1
Def		(f1,f2) o g	[compose2]	graph 1 1
Def		Bij(A; B; f)	[biject]	fun 1
Def		P Q	[rev_implies]	core
Def		isl(x)	[isl]	union
Def		outl(x)	[outl]	union
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		hd(l)	[hd]	list 1
Def		ij	[le_int]	bool 1
Def		i < j	[lt_int]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		p q	[bor]	bool 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		map(f;as)	[map]	list 1
Def		tl(l)	[tl]	list 1
Def		b	[bnot]	bool 1

About: