Def		t.eqw	[gro_eqw]	graph 1 3
Def		t.eaccw	[gro_eaccw]	graph 1 3
Def		t.vaccw	[gro_vaccw]	graph 1 3
Def		t.other	[gro_other]	graph 1 3
Def		For any graph representation P(the_graph;the_obj)	[allgrep]	graph 1 3
Def		adjm-rep{\\\\v:l,i:l}()	[adjm-rep]	graph 1 3
Def		AdjListRep	[adjl-rep]	graph 1 3
Def		adjl_to_adjm(l)	[adjl_to_adjm]	graph 1 3
Def		array[n]:=v	[array-const]	graph 1 2
Def		t.o	[gr_o]	graph 1 2
Def		union-reduce(f;g;x;as)	[union-reduce]	graph 1 1
Def		vertex-count(the_obj;x.P(x))	[vertex-count]	graph 1 3
Def		Dec(P)	[decidable]	core
Def		l_disjoint(T;l1;l2)	[l_disjoint]	mb list 2
Def		Prop	[prop]	core
Def		depthfirst-traversal(the_graph;s)	[depthfirst-traversal]	graph 1 2
Def		topsort(G)	[topsort]	graph 1 3
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		dfsl-traversal(the_graph;L;s)	[dfsl-traversal]	graph 1 2
Def		topsortl(A;L)	[topsortl]	graph 1 3
Def		topsortedl(the_graph;L;s)	[topsortedl]	graph 1 2
Def		adjm_to_adjl(m)	[adjm_to_adjl]	graph 1 3
Def		G H	[graph-isomorphic]	graph 1 2
Def		mod_guard(x;y)	[mod_guard]	graph 1 2
Def		prime(a)	[prime]	num thy 1
Def			[int_nzero]	int 1
Def		f[n:=x]	[fappend]	mb nat
Def		Bij(A; B; f)	[biject]	fun 1
Def		Inj(A; B; f)	[inject]	fun 1
Def		i > j	[gt]	core
Def		r- > L^k	[arrows]	graph 1 2
Def		L[i--]	[list-dec]	graph 1 2
Def		{T}	[guard]	core
Def		member-right-paren(x,y.E(x;y);i;s)	[member-right-paren]	graph 1 2
Def		member-left-paren(x,y.E(x;y);i;s)	[member-left-paren]	graph 1 2
Def		a[i:=v]	[array-update]	graph 1 2
Def		array(T)	[array]	graph 1 2
Def		array-count(v.P(v);a)	[array-count]	graph 1 2
Def		L1-G- > *L2	[list-list-connect]	graph 1 2
Def		x before y l	[l_before]	mb list 1
Def		L1 L2	[sublist]	mb list 1
Def		Graph Representation	[graphrep]	graph 1 3
Def		GraphObject(the_graph)	[graphobj]	graph 1 3
Def		no_repeats(T;l)	[no_repeats]	mb list 2
Def		L-G- > *x	[list-connect]	graph 1 2
Def		(xL.P(x))	[l_exists]	mb list 2
Def		(xL.P(x))	[l_all]	mb list 2
Def		df-traversal(G;s)	[df-traversal]	graph 1 2
Def		(x l)	[l_member]	mb list 1
Def		adjl-graph(G)	[adjl-graph]	graph 1 3
Def		non-trivial-loop(G;i)	[non-trivial-loop]	graph 1 2
Def		x-the_graph- > *y	[connect]	graph 1 2
Def		last(L)	[last]	mb list 1
Def		path(the_graph;p)	[path]	graph 1 2
Def		l[i]	[select]	list 1
Def		nth_tl(n;as)	[nth_tl]	list 1
Def		tl(l)	[tl]	list 1
Def		l1 l2	[iseg]	mb list 1
Def		EquivRel x,y:T. E(x;y)	[equiv_rel]	rel 1
Def		DivGraph_2	[divides-graph2]	graph 1 2
Def		DivGraph_1	[divides-graph1]	graph 1 2
Def		(xL.P(x))	[l_ball]	graph 1 1
Def		InvFuns(A; B; f; g)	[inv_funs]	fun 1
Def		Graph(x,y:T. R(x;y))	[rel-graph]	graph 1 2
Def		Id	[tidentity]	fun 1
Def		Id	[identity]	fun 1
Def		firstn(n;as)	[firstn]	list 1
Def		{i...j}	[int_iseg]	int 1
Def		process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; }	[accumulate]	graph 1 1
Def		rev(as)	[reverse]	list 1
Def		|i|	[absval]	int 2
Def		f91(i)	[f91]	graph 1 1
Def		a n	[div_floor]	int 2
Def		Graph	[graph]	graph 1 2
Def		Top	[top]	core
Def		dfsl(G;L)	[dfsl]	graph 1 3
Def		adjl-obj{\\\\v:l,i:l}(A)	[adjl-obj]	graph 1 3
Def		adjl-edge-accum(A;s',x'.f(s';x');s;x)	[adjl-edge-accum]	graph 1 3
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		adjm-graph(A)	[adjm-graph]	graph 1 3
Def		b	[assert]	bool 1
Def		P Q	[iff]	core
Def		x:A. B(x)	[all]	core
Def			[bool]	bool 1
Def		traversal(G)	[traversal]	graph 1 2
Def		Vertices(t)	[gr_v]	graph 1 2
Def		vertex-subset(the_obj;x.P(x))	[vertex-subset]	graph 1 3
Def		depthfirst(the_obj)	[depthfirst]	graph 1 3
Def		t.vacc	[gro_vacc]	graph 1 3
Def		t.graph	[grr_graph]	graph 1 3
Def		t.type	[grr_type]	graph 1 3
Def		dfs(the_obj;s;i)	[dfs]	graph 1 3
Def		t.eacc	[gro_eacc]	graph 1 3
Def		t.eq	[gro_eq]	graph 1 3
Def		adjm-obj{\\\\v:l,i:l}(M)	[adjm-obj]	graph 1 3
Def		adjm-vertex-accum(M;s',x.f(s';x);s)	[adjm-vertex-accum]	graph 1 3
Def		adjm-edge-accum(M;s',x'.f(s';x');s;x)	[adjm-edge-accum]	graph 1 3
Def		t.size	[adjm_size]	graph 1 3
Def		adjl-vertex-accum(A;s',x.f(s';x);s)	[adjl-vertex-accum]	graph 1 3
Def		t.size	[adjl_size]	graph 1 3
Def		|a|	[array-length]	graph 1 2
Def		Incidence(t)	[gr_f]	graph 1 2
Def		Edges(t)	[gr_e]	graph 1 2
Def		< x,y > .P(x;y)	[plambda]	graph 1 1
Def		Graph(a:A -- > f(a;b) | b:B)	[fun-graph]	graph 1 2
Def		1of(t)	[pi1]	core
Def		t.obj	[grr_obj]	graph 1 3
Def		t.adj	[adjm_adj]	graph 1 3
Def		t.out	[adjl_out]	graph 1 3
Def		a[i]	[array-select]	graph 1 2
Def		2of(t)	[pi2]	core
Def		if b t else f fi	[ifthenelse]	bool 1
Def		paren(T;s)	[paren]	graph 1 2
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		AdjMatrix	[adjmatrix]	graph 1 3
Def		AdjList	[adjlist]	graph 1 3
Def		increasing(f;k)	[increasing]	mb basic
Def		{i..j}	[int_seg]	int 1
Def			[nat]	int 1
Def			[it]	core
Def		< vertices = v, edges = e, incidence = f >	[mkgraph]	graph 1 2
Def		mklist(n;f)	[mklist]	mb list 1
Def		sum(f(x) | x < k)	[sum]	mb nat
Def		primrec(n;b;c)	[primrec]	mb nat
Def		x =M= y	[eq_adjm]	graph 1 3
Def		x =A= y	[eq_adjl]	graph 1 3
Def		a mod n	[modulus]	int 2
Def		i=j	[eq_int]	bool 1
Def		mkgraphobj(eq, eqw, eacc, eaccw, vacc, vaccw, other)	[mkgraphobj]	graph 1 3
Def		mkgraphrep(type, graph, obj)	[mkgraphrep]	graph 1 3
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]	graph 1 3
Def		Case mk_adjmatrix(size,adj) = > body(size;adj)	[case_mk_adjmatrix]	graph 1 3
Def		Case(value) body	[case]	prog 1
Def		(xL.P(x))	[l_bexists]	graph 1 1
Def		mk_adjmatrix(size, adj)	[mk_adjmatrix]	graph 1 3
Def		Case mk_adjlist(size; out ) = > body(size;out)	[case_mk_adjlist]	graph 1 3
Def		map(f;as)	[map]	list 1
Def		A & B	[cand]	core
Def		i j < k	[lelt]	int 1
Def		AB	[le]	core
Def		P Q	[implies]	core
Def		as @ bs	[append]	list 1
Def		P Q	[or]	core
Def		false	[bfalse]	bool 1
Def		a b	[nequal]	core
Def		A	[not]	core
Def		f o g	[compose]	fun 1
Def		(f1,f2) o g	[compose2]	graph 1 1
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def			[nat_plus]	int 1
Def		true	[btrue]	bool 1
Def		pq	[band]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		p q	[bor]	bool 1
Def		ij	[le_int]	bool 1
Def		i < j	[lt_int]	bool 1
Def		isl(x)	[isl]	union
Def		outl(x)	[outl]	union
Def		Trans x,y:T. E(x;y)	[trans]	rel 1
Def		Sym x,y:T. E(x;y)	[sym]	rel 1
Def		Refl(T;x,y.E(x;y))	[refl]	rel 1
Def		P Q	[rev_implies]	core
Def		hd(l)	[hd]	list 1
Def		Surj(A; B; f)	[surject]	fun 1
Def		b	[bnot]	bool 1

About: