Def		array[n]:=v	[array-const]
Def		t.o	[gr_o]
Def		non-trivial-loop-free(G)	[non-trivial-loop-free]
Def		topsorted(the_graph;s)	[topsorted]
Def		topsortedl(the_graph;L;s)	[topsortedl]
Def		mod_guard(x;y)	[mod_guard]
Def		prime(a)	[prime]	num thy 1
Def			[int_nzero]	int 1
Def		f[n:=x]	[fappend]	mb nat
Def		G H	[graph-isomorphic]
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]
Def		Prop	[prop]	core
Def		L[i--]	[list-dec]
Def		{T}	[guard]	core
Def		member-paren(x,y.E(x;y);i;s)	[member-paren]
Def		b	[assert]	bool 1
Def			[bool]	bool 1
Def		member-right-paren(x,y.E(x;y);i;s)	[member-right-paren]
Def		member-left-paren(x,y.E(x;y);i;s)	[member-left-paren]
Def		no_repeats(T;l)	[no_repeats]	mb list 2
Def		Dec(P)	[decidable]	core
Def		a[i:=v]	[array-update]
Def		array(T)	[array]
Def		array-count(v.P(v);a)	[array-count]
Def		Graph	[graph]
Def		L1-G- > *L2	[list-list-connect]
Def		depthfirst-traversal(the_graph;s)	[depthfirst-traversal]
Def		dfl-traversal(the_graph;L;s)	[dfl-traversal]
Def		dfsl-traversal(the_graph;L;s)	[dfsl-traversal]
Def		L-G- > *x	[list-connect]
Def		df-traversal(G;s)	[df-traversal]
Def		non-trivial-loop(G;i)	[non-trivial-loop]
Def		x-the_graph- > *y	[connect]
Def		last(L)	[last]	mb list 1
Def		path(the_graph;p)	[path]
Def		(xL.P(x))	[l_exists]	mb list 2
Def		(xL.P(x))	[l_all]	mb list 2
Def		(x l)	[l_member]	mb list 1
Def		x before y l	[l_before]	mb list 1
Def		L1 L2	[sublist]	mb list 1
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]
Def		DivGraph_1	[divides-graph1]
Def		a mod n	[modulus]	int 2
Def		map(f;as)	[map]	list 1
Def		increasing(f;k)	[increasing]	mb basic
Def		A & B	[cand]	core
Def		x:A. B(x)	[exists]	core
Def		paren(T;s)	[paren]
Def		||as||	[length]	list 1
Def		P & Q	[and]	core
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		x:A. B(x)	[all]	core
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		i=j	[eq_int]	bool 1
Def		if b t else f fi	[ifthenelse]	bool 1
Def		as @ bs	[append]	list 1
Def		P Q	[or]	core
Def		Y	[ycomb]	core
Def		(xL.P(x))	[l_bexists]	graph 1 1
Def		false	[bfalse]	bool 1
Def		|a|	[array-length]
Def		x-the_graph- > y	[edge]
Def		Incidence(t)	[gr_f]
Def		traversal(G)	[traversal]
Def		Vertices(t)	[gr_v]
Def		Edges(t)	[gr_e]
Def		< x,y > .P(x;y)	[plambda]	graph 1 1
Def		Graph(x,y:T. R(x;y))	[rel-graph]
Def		Graph(a:A -- > f(a;b) | b:B)	[fun-graph]
Def		1of(t)	[pi1]	core
Def		a[i]	[array-select]
Def		2of(t)	[pi2]	core
Def		Top	[top]	core
Def		a b	[nequal]	core
Def		A	[not]	core
Def		P Q	[iff]	core
Def		f o g	[compose]	fun 1
Def		(f1,f2) o g	[compose2]	graph 1 1
Def			[it]	core
Def		Id	[tidentity]	fun 1
Def		< vertices = v, edges = e, incidence = f >	[mkgraph]
Def		a ~ b	[assoced]	num thy 1
Def		b | a	[divides]	num thy 1
Def			[nat_plus]	int 1
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		ij	[le_int]	bool 1
Def		hd(l)	[hd]	list 1
Def		p q	[bor]	bool 1
Def		reduce(f;k;as)	[reduce]	list 1
Def		P Q	[rev_implies]	core
Def		Surj(A; B; f)	[surject]	fun 1
Def		Id	[identity]	fun 1
Def		i < j	[lt_int]	bool 1
Def		b	[bnot]	bool 1

About: