[Imprint][Data Privacy Statement][E-Mail]

Back to the index. View project statistic. View project symbols. View KIV symbols to check that all symbols are available.

All project symbols

symbol	specification	entry
#	array	function, array → nat
#	stream-of-streams	function, streamstream → natinf
#	stream-of-streams	function, streamlist → nat
#	matrixops	function, vector → nat
#	assoclist	function, assoclist → nat
#	stream	function, stream → natinf
#	string	function, string → nat
#	list-data	function, list → nat
#	set-basic	function, set → nat
#	natstream	function, natstream → natinf
#	natstream	function, natlist → nat
#	store	function, store → nat
#	bag-union	function, bag → nat
#	natset	function, natset → nat
#	reflist	function, reflist → nat
#	linheap	function, heap → nat
#c	matrix	function, matrix → nat
#oc	list-perm	function, elem × list → nat
#oc	list-as-arrayinstance	function, elem × array → nat
#r	matrix	function, matrix → nat
%	nat-div	partial function, nat × nat → nat
%	int-div	partial function, int × int → int
'	stream-of-streams	function, stream → streamlist
'	list	function, elem → list
'	assoclist	function, pair → assoclist
'	string	function, char → string
'	natstream	function, nat → natlist
'	list-as-arrayinstance	function, elem → array
'	reflist	function, Ref → reflist
*	nat-mult	function, nat × nat → nat
*	matrixops	partial function, vector × vector → elem
*	matrixops	partial function, vector × matrix → vector
*	matrixops	partial function, matrix × vector → vector
*	matrixops	partial function, matrix × matrix → matrix
*	ring	function, elem × elem → elem
*	int-mult	function, int × int → int
+	array-listops	function, elem × array → array
+	stream-of-streams	function, streamstream × streamstream → streamstream
+	stream-of-streams	function, stream × streamstream → streamstream
+	stream-of-streams	function, streamlist × stream → streamlist
+	stream-of-streams	function, streamlist × streamlist → streamlist
+	stream-of-streams	function, stream × streamlist → streamlist
+	int-basic2	function, int × int → int
+	matrixops	partial function, vector × vector → vector
+	matrixops	partial function, matrix × matrix → matrix
+	nat-inf	function, natinf × natinf → natinf
+	ring	function, elem × elem → elem
+	list	function, list × elem → list
+	list	function, list × list → list
+	assoclist	function, assoclist × pair → assoclist
+	assoclist	function, assoclist × assoclist → assoclist
+	assoclist	function, pair × assoclist → assoclist
+	stream	function, stream × stream → stream
+	stream	function, elem × stream → stream
+	string	function, string × char → string
+	string	function, string × string → string
+	string	function, char × string → string
+	list-data	function, elem × list → list
+	natstream	function, natstream × natstream → natstream
+	natstream	function, nat × natstream → natstream
+	natstream	function, natlist × nat → natlist
+	natstream	function, natlist × natlist → natlist
+	natstream	function, nat × natlist → natlist
+	list-as-arrayinstance	function, array × elem → array
+	list-as-arrayinstance	function, array × array → array
+	nat-basic	function, nat × nat → nat
+	reflist	function, reflist × Ref → reflist
+	reflist	function, reflist × reflist → reflist
+	reflist	function, Ref × reflist → reflist
++	stream-of-streams	function, streamlist × stream → streamlist
++	list-dup	function, list × elem → list
++	assoclist	function, assoclist × pair → assoclist
++	string	function, string × char → string
++	set-basic	function, set × elem → set
++	natstream	function, natlist × nat → natlist
++	bag-basic	function, bag × elem → bag
++	infset-basic	function, set × elem → set
++	list-as-arrayinstance	function, array × elem → array
++	natset	function, natset × nat → natset
++	reflist	function, reflist × Ref → reflist
+1	nat-basic	function, nat → nat
+1	int-basic1	function, int → int
+2	list	function, elem × elem → list
+2	assoclist	function, pair × pair → assoclist
+2	string	function, char × char → string
+2	list-as-arrayinstance	function, elem × elem → array
+2	reflist	function, Ref × Ref → reflist
+l	stream-of-streams	function, stream × stream → streamlist
+l	natstream	function, nat × nat → natlist
-	int-abs	function, int × int → int
-	nat	partial function, nat × nat → nat
--	store	function, store × elem → store
--	set-union	function, set × elem → set
--	bag-union	function, bag × elem → bag
--	infset-union	function, set × elem → set
--	natset	function, natset × nat → natset
--	linheap	function, heap × Ref → heap
-1	nat-basic	partial function, nat → nat
-1	int-basic1	function, int → int
-1l	list-del	function, list × elem → list
-1l	stream-of-streams	function, streamlist × stream → streamlist
-1l	assoclist	function, assoclist × pair → assoclist
-1l	string	function, string × char → string
-1l	natstream	function, natlist × nat → natlist
-1l	list-as-arrayinstance	function, array × elem → array
-1l	reflist	function, reflist × Ref → reflist
-l	list-del	function, list × elem → list
-l	stream-of-streams	function, streamlist × stream → streamlist
-l	assoclist	function, assoclist × pair → assoclist
-l	string	function, string × char → string
-l	natstream	function, natlist × nat → natlist
-l	list-as-arrayinstance	function, array × elem → array
-l	reflist	function, reflist × Ref → reflist
-p	list-del	function, list × nat → list
-p	stream-of-streams	function, streamlist × nat → streamlist
-p	assoclist	function, assoclist × nat → assoclist
-p	string	function, string × nat → string
-p	list-as-arrayinstance	function, array × nat → array
-p	reflist	function, reflist × nat → reflist
-pos	natstream	function, natlist × nat → natlist
-∞	int-inf-basic	constant, intinf
.1	nat-pair	function, nat → nat
.1	pair	function, pair → elem
.1	int-pair	function, int → int
.2	nat-pair	function, nat → nat
.2	pair	function, pair → data
.2	int-pair	function, int → int
.butlast	stream-of-streams	partial function, streamlist → streamlist
.butlast	assoclist	partial function, assoclist → assoclist
.butlast	string	partial function, string → string
.butlast	list-last	partial function, list → list
.butlast	natstream	partial function, natlist → natlist
.butlast	list-as-arrayinstance	partial function, array → array
.butlast	reflist	partial function, reflist → reflist
.butmax	oset	partial function, set → set
.butmin	oset	partial function, set → set
.butmin	ostore	partial function, store → store
.char1	string	partial function, string → char
.f	stream-of-streams	partial function, streamstream → nat → stream
.f	stream-basic	partial function, stream → nat → elem
.f	natstream	partial function, natstream → nat → nat
.first	array-listops	partial function, array → elem
.head	stream-of-streams	partial function, streamlist → stream
.head	assoclist	partial function, assoclist → pair
.head	list-data	partial function, list → elem
.head	natstream	partial function, natlist → nat
.i	int-inf-basic	partial function, intinf → int
.keys	ostore	function, store → set
.l	stream-of-streams	partial function, streamstream → streamlist
.l	stream-basic	partial function, stream → list
.l	natstream	partial function, natstream → natlist
.last	stream-of-streams	partial function, streamlist → stream
.last	assoclist	partial function, assoclist → pair
.last	string	partial function, string → char
.last	list-last	partial function, list → elem
.last	natstream	partial function, natlist → nat
.last	list-as-arrayinstance	partial function, array → elem
.last	reflist	partial function, reflist → Ref
.map	store-map	function, store × elem × data → data → store
.map	store-map	function, store × data → data → store
.max	oset	partial function, set → elem
.min	oset	partial function, set → elem
.min	ostore	partial function, store → elem
.n	nat-inf	partial function, natinf → nat
.nxt	lincell	function, cell → Ref
.rest	array-listops	partial function, array → array
.rstring	string	partial function, string → string
.tail	stream-of-streams	partial function, streamlist → streamlist
.tail	assoclist	partial function, assoclist → assoclist
.tail	list-data	partial function, list → list
.tail	natstream	partial function, natlist → natlist
.toArc	rowcol-upd	function, matrix → array
.toArr	rowcol-upd	function, matrix → array
/	nat-div	partial function, nat × nat → nat
/	int-div	partial function, int × int → int
2^	nat-pot	function, nat → nat
<	array-listops	predicate, array × array
<	oset	predicate, set × elem
<	oset	predicate, elem × set
<	stream-of-streams	predicate, streamlist × streamlist
<	oelem	predicate, elem × elem
<	nat-inf	predicate, natinf × natinf
<	int-inf	predicate, intinf × intinf
<	assoclist	predicate, assoclist × assoclist
<	list-data	predicate, list × list
<	natstream	predicate, natlist × natlist
<	string-less	predicate, char × char
<	string-less	predicate, string × string
<	nat-basic	predicate, nat × nat
<	reflist	predicate, reflist × reflist
<	int-basic1	predicate, int × int
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
A	wellfounded-TL	variable, elem,flexible
I	ring	constant, elem
IS	monotone-set-fixpoint	function, (elem → bool) → bool → elem → bool
N	wellfounded-TL	variable, nat,flexible
O	ring	constant, elem
O-	matrixops	function, vector → vector
O-	matrixops	function, matrix → matrix
O-	ring	function, elem → elem
Ref	Ref	sort,
UN	monotone-set-fixpoint	function, (elem → bool) → bool → elem → bool
[]	array-listops	constant, array
[]	stream-of-streams	constant, streamstream
[]	stream-of-streams	constant, streamlist
[]	assoclist	constant, assoclist
[]	stream	constant, stream
[]	list-data	constant, list
[]	natstream	constant, natstream
[]	natstream	constant, natlist
[]	reflist	constant, reflist
\	set-union	function, set × set → set
\	list-as-arrayinstance	function, array × array → array
\	bag-union	function, bag × bag → bag
\	infset-union	function, set × set → set
\	natset	function, natset × natset → natset
\	list-set	function, list × list → list
\	reflist	function, reflist × reflist → reflist
\	store+set	function, store × set → store
]	list-getput	partial function, list × nat × elem → list
]	list-getput	partial function, list × nat → elem
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	stream-of-streams	partial function, streamstream × nat × stream → streamstream
]	stream-of-streams	partial function, streamstream × nat → stream
]	stream-of-streams	partial function, streamlist × nat × stream → streamlist
]	stream-of-streams	partial function, streamlist × nat → stream
]	matrixops	partial function, vector × nat × elem → vector
]	matrixops	partial function, vector × nat → elem
]	assoclist	partial function, assoclist × data → elem
]	assoclist	partial function, assoclist × elem → data
]	assoclist	partial function, assoclist × nat × pair → assoclist
]	assoclist	partial function, assoclist × nat → pair
]	assoclist	function, assoclist × elem × data → assoclist
]	stream	partial function, stream × nat × elem → stream
]	stream	partial function, stream × nat → elem
]	matrix	partial function, matrix × nat × nat × elem → matrix
]	matrix	partial function, matrix × nat × nat → elem
]	string	partial function, string × nat × char → string
]	string	partial function, string × nat → char
]	natstream	partial function, natstream × nat × nat → natstream
]	natstream	partial function, natstream × nat → nat
]	natstream	partial function, natlist × nat × nat → natlist
]	natstream	partial function, natlist × nat → nat
]	store	partial function, store × elem → data
]	store	function, store × elem × data → store
]	reflist	partial function, reflist × nat × Ref → reflist
]	reflist	partial function, reflist × nat → Ref
]	linheap	partial function, heap × Ref → cell
]	linheap	function, heap × Ref × cell → heap
]c	matrixops	partial function, matrix × nat → vector
]c	rowcol-upd	partial function, matrix × nat × array → matrix
]c	matrix+array	partial function, matrix × nat → array
]r	matrixops	partial function, matrix × nat → vector
]r	rowcol-upd	partial function, matrix × nat × array → matrix
]r	matrix+array	partial function, matrix × nat → array
^	approx-fixpoint	function, (elem → bool) → elem → bool × nat → (elem → bool) → elem → bool
^	nat-pot	function, nat × nat → nat
^	int-pot	partial function, int × int → int
^*	rtc	function, elem × elem → bool → elem × elem → bool
^2	int-square	function, int → int
a	list-getput	variable, elem
a	hilbert-choice	variable, elem
a	array-listops	variable, elem
a	putoutside-id	variable, elem
a	array	variable, elem
a	list-del	variable, elem
a	olist	variable, elem
a	wellfounded	variable, elem
a	oelem	variable, elem
a	list-perm	variable, elem
a	store-map	variable, elem
a	matrixops	variable, elem
a	filter-count	variable, elem
a	wellfounded-TL	variable, elem
a	list-dup	variable, elem
a	ring	variable, elem
a	array-copy	variable, elem
a	list	variable, elem
a	assoclist	variable, elem
a	infinite-append	variable, elem
a	list-setequal	variable, elem
a	olist-min-max	variable, elem
a	stream	variable, elem
a	elem	variable, elem
a	choice	variable, elem
a	lexical	variable, elem1
a	matrix	variable, elem
a	pair	variable, elem
a	list-data	variable, elem
a	array-revin	variable, elem
a	inf-app-list	variable, elem
a	list-last	variable, elem
a	rowcol-upd	variable, array
a	bag-basic	variable, elem
a	mon-lim-filter-count	variable, elem
a	infset-basic	variable, elem
a	olist-sort	variable, elem
a	bag-union	variable, elem
a	infset-union	variable, elem
a	list-set	variable, elem
a	store+set	variable, elem
a0	wellfounded	variable, elem
a1	wellfounded	variable, elem
aa	choice	constant, elem
abs	int-abs	function, int → int
ar	array-listops	variable, array
ar	array	variable, array
ar	array-copy	variable, array
ar	array-revin	variable, array
ar	get-outside	variable, array
array	array	sort,
assoclist	assoclist	sort,
ax	assoclist	variable, assoclist
ay	assoclist	variable, assoclist
az	assoclist	variable, assoclist
b	list-getput	variable, elem
b	list-del	variable, elem
b	olist	variable, elem
b	list-perm	variable, elem
b	filter-count	variable, elem
b	list-dup	variable, elem
b	ring	variable, elem
b	list	variable, elem
b	assoclist	variable, elem
b	list-setequal	variable, elem
b	elem	variable, elem
b	choice	variable, elem
b	lexical	variable, elem2
b	inf-app-list	variable, elem
b	list-last	variable, elem
b	bag-basic	variable, elem
b	mon-lim-filter-count	variable, elem
b	infset-basic	variable, elem
b	olist-sort	variable, elem
b	bag-union	variable, elem
b	infset-union	variable, elem
b	list-set	variable, elem
bag	bag-basic	variable, bag
bag	bag-basic	sort,
bag	bag-union	variable, bag
bool	bool	sort,
boolvar	bool	variable, bool
butlastn	stream-of-streams	partial function, nat × streamlist → streamlist
butlastn	assoclist	partial function, nat × assoclist → assoclist
butlastn	string	partial function, nat × string → string
butlastn	list-last	partial function, nat × list → list
butlastn	natstream	partial function, nat × natlist → natlist
butlastn	list-as-arrayinstance	partial function, nat × array → array
butlastn	reflist	partial function, nat × reflist → reflist
c	list-getput	variable, elem
c	list-del	variable, elem
c	olist	variable, elem
c	list-perm	variable, elem
c	matrixops	variable, nat
c	list-dup	variable, elem
c	ring	variable, elem
c	list	variable, elem
c	celem	constant, elem
c	list-setequal	variable, elem
c	elem	variable, elem
c	choice	variable, elem
c	matrix	variable, nat
c	list-last	variable, elem
c	rowcol-upd	variable, nat
c	olist-sort	variable, elem
c	infset-union	variable, elem
c	matrix+array	variable, nat
c	list-set	variable, elem
ce	path-reachable	variable, cell
ce	lincell	variable, cell
cell	lincell	sort,
chain	approx-fixpoint	predicate, nat → elem → bool
char	char	variable, char
char	char	sort,
char	string-less	variable, char
chn	approx-fixpoint	variable, nat → elem → bool
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
cmp	array-copy	predicate, array × elem
cnt	natstream	function, nat × natstream → natinf
cnt	mon-lim-filter-count	function, elem × stream → natinf
compl	monotone-set-fixpoint	function, (elem → bool) → elem → bool → (elem → bool) → elem → bool
cont	approx-fixpoint	predicate, (elem → bool) → elem → bool
copy	array-copy	partial function, array × nat × array × nat × nat → array
count	filter-count	partial function, list × nat × nat × elem → bool → nat
count	filter-count	function, list × elem → bool → nat
count	oarray-sort	partial function, array × nat × nat × elem → bool → nat
count	oarray-sort	function, array × elem → bool → nat
count	bag-basic	function, elem × bag → nat
d	assoclist	variable, data
d	pair	variable, data
d	data	variable, data
d	store+set	variable, data
data	data	sort,
dataf	store-map	variable, data → data
decode	int-pair	function, int → nat
decode	int-pair	function, nat → int
disj	stream-of-streams	predicate, streamlist × streamlist
disj	list-dup	predicate, list × list
disj	assoclist	predicate, assoclist × assoclist
disj	string	predicate, string × string
disj	natstream	predicate, natlist × natlist
disj	list-as-arrayinstance	predicate, array × array
disj	reflist	predicate, reflist × reflist
dist	nat-prime	function, nat × nat → nat
dom	store+set	function, store → set
dups	stream-of-streams	predicate, streamlist
dups	list-dup	predicate, list
dups	assoclist	predicate, assoclist
dups	string	predicate, string
dups	natstream	predicate, natlist
dups	list-as-arrayinstance	predicate, array
dups	reflist	predicate, reflist
elem	hilbert-choice	sort,
elem	wellfounded	sort,
elem	elem	sort,
elem	setelems	sort,
elem1	lexical-param	sort,
elem2	lexical-param	sort,
elemdataf	store-map	variable, elem × data → data
elemf	choice	variable, elem → elem
encode	nat-pair	function, nat × nat → nat
encode	int-pair	function, nat → int
encode	int-pair	function, int → nat
even	int-min	predicate, int
even	nat-even	predicate, nat
f	matrixops	variable, nat → elem
f	stream-basic	variable, nat → elem
f	approx-fixpoint	variable, (elem → bool) → elem → bool
f	infset-basic	variable, elem → bool
f	monotone-set-fixpoint	variable, (elem → bool) → elem → bool
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
fillfirst	stream-of-streams	function, nat × stream × streamlist → streamlist
fillfirst	assoclist	function, nat × pair × assoclist → assoclist
fillfirst	string	function, nat × char × string → string
fillfirst	list-last	function, nat × elem × list → list
fillfirst	natstream	function, nat × nat × natlist → natlist
fillfirst	list-as-arrayinstance	function, nat × elem × array → array
fillfirst	reflist	function, nat × Ref × reflist → reflist
filter	filter-count	function, list × elem → bool → list
filter	oarray-sort	function, array × elem → bool → array
filter	natstream	function, nat → bool × natstream → natstream
filter	mon-lim-filter-count	function, elem → bool × stream → stream
filter	list-as-arrayinstance	function, array × array → array
filter	list-set	function, list × list → list
filter	reflist	function, reflist × reflist → reflist
finp	stream-of-streams	predicate, streamstream
finp	stream-basic	predicate, stream
finp	natstream	predicate, natstream
firstn	list-del	partial function, nat × list → list
firstn	stream-of-streams	partial function, nat × streamlist → streamlist
firstn	assoclist	partial function, nat × assoclist → assoclist
firstn	string	partial function, nat × string → string
firstn	natstream	partial function, nat × natlist → natlist
firstn	list-as-arrayinstance	partial function, nat × array → array
firstn	reflist	partial function, nat × reflist → reflist
from	stream-of-streams	partial function, streamlist × nat → streamlist
from	stream-of-streams	partial function, streamstream × nat → streamstream
from	stream-of-streams	function, nat → stream × nat → nat → stream
from	stream	partial function, list × nat → list
from	stream	partial function, stream × nat → stream
from	stream	function, nat → elem × nat → nat → elem
from	natstream	partial function, natlist × nat → natlist
from	natstream	partial function, natstream × nat → natstream
from	natstream	function, nat → nat × nat → nat → nat
frome	list-del	function, list × elem → list
frome	stream-of-streams	function, streamlist × stream → streamlist
frome	assoclist	function, assoclist × pair → assoclist
frome	string	function, string × char → string
frome	natstream	function, natlist × nat → natlist
frome	list-as-arrayinstance	function, array × elem → array
frome	reflist	function, reflist × Ref → reflist
g	matrixops	variable, nat × nat → elem
gcd	nat-prime	function, nat × nat → nat
gcd	int-gcd	function, int × int → int
h	path-reachable	variable, heap
hd	stream-of-streams	partial function, streamstream → stream
hd	stream	partial function, stream → elem
hd	natstream	partial function, natstream → nat
hd	reflist	partial function, reflist → Ref
head	list-data	variable, elem
heap	linheap	sort,
i	int-div	variable, int
i	int-basic2	variable, int
i	int-inf-basic	variable, int
i	intnat	variable, int
i	int-inf	variable, int
i	int-min	variable, int
i	rowcol-upd	variable, elem
i	int-abs	variable, int
i	int-pot	variable, int
i	int-square	variable, int
i	int-pair	variable, int
i	int-gcd	variable, int
i	int-mult	variable, int
i	int-basic1	variable, int
iHP	wellfounded	variable, elem → bool
iHPQ	lexical	variable, elem1 × elem2 → bool
idrange	array-copy	partial predicate, array × nat × nat
id○	array-copy	predicate, array × array × nat × nat
id○	array-copy	predicate, array × array × nat
ii	infinite-append	variable, nat → nat
ii	inf-app-list	variable, nat → nat
iigen	infinite-append	variable, nat → nat → nat
ins≤	olist	function, elem × list → list
ins≤	oarray-sort	function, elem × array → array
int	int-basic1	sort,
intinf	int-inf-basic	sort,
inv	rtc-rel	predicate, elem × elem → bool
inv	stut-mon	partial function, natstream → natstream
iset	approx-fixpoint	variable, elem → bool
iset	monotone-set-fixpoint	variable, elem → bool
isetset	monotone-set-fixpoint	variable, (elem → bool) → bool
i→n	intnat	function, int → nat
i∞	int-inf-basic	variable, intinf
i∞	int-inf	variable, intinf
j	int-div	variable, int
j	int-basic2	variable, int
j	intnat	variable, int
j	int-min	variable, int
j	rowcol-upd	variable, elem
j	int-abs	variable, int
j	int-pot	variable, int
j	int-square	variable, int
j	int-pair	variable, int
j	int-gcd	variable, int
j	int-mult	variable, int
j	int-basic1	variable, int
jj	infinite-append	variable, nat → nat
l	stream-basic	variable, list
lastn	list-del	partial function, nat × list → list
lastn	stream-of-streams	partial function, nat × streamlist → streamlist
lastn	assoclist	partial function, nat × assoclist → assoclist
lastn	string	partial function, nat × string → string
lastn	natstream	partial function, nat × natlist → natlist
lastn	list-as-arrayinstance	partial function, nat × array → array
lastn	reflist	partial function, nat × reflist → reflist
lastoc	natstream	function, nat × natstream → natinf
lastoc	mon-lim-filter-count	function, elem × stream → natinf
leninv	stut-mon	function, natstream → natinf
lex<	lexical	predicate, elem1 × elem2 × elem1 × elem2
lf	infinite-append	variable, nat → list
lf	inf-app-list	variable, nat → list
lfgen	infinite-append	variable, nat → nat → list
lim	natstream	partial function, nat → natstream → natstream
lim	mon-lim-filter-count	partial function, nat → stream → stream
lim	streamseq-mon-lim	partial function, streamstream → stream
list	list-data	sort,
log	nat-pot	partial function, nat × nat → nat
log2	nat-pot	partial function, nat → nat
m	list-getput	variable, nat
m	nat-div	variable, nat
m	array	variable, nat
m	list-del	variable, nat
m	nat-mult	variable, nat
m	list-perm	variable, nat
m	matrixops	variable, nat
m	filter-count	variable, nat
m	intnat	variable, nat
m	nat-inf	variable, nat
m	nat-pair	variable, nat
m	stream-basic	variable, nat
m	array-copy	variable, nat
m	infinite-append	variable, nat
m	choice	variable, nat
m	array-revin	variable, nat
m	inf-app-list	variable, nat
m	approx-fixpoint	variable, nat
m	list-last	variable, nat
m	rowcol-upd	variable, nat
m	nat-sgn	variable, nat
m	nat-pot	variable, nat
m	mon-lim-filter-count	variable, nat
m	path-reachable	variable, nat
m	int-pair	variable, nat
m	nat-even	variable, nat
m	natset	variable, nat
m	streamseq-mon-lim	variable, nat
m	list-set	variable, nat
matrix	matrix	sort,
max	oelem-min-max	function, elem × elem → elem
max	olist-min-max	partial function, list → elem
max	int-min	function, int × int → int
max	oarray-sort	partial function, array → elem
max	nat-even	function, nat × nat → nat
max_prime_divisor	int-gcd	function, int → int
maxenc	nat-pair	function, nat × nat → nat
maxenc	nat-pair	function, nat → nat
max∞	stut-mon	function, nat → bool → natinf
merge	olist	function, list × list → list
merge	oarray-sort	function, array × array → array
min	nat-inf	function, natinf × natinf → natinf
min	oelem-min-max	function, elem × elem → elem
min	olist-min-max	partial function, list → elem
min	int-min	function, int × int → int
min	oarray-sort	partial function, array → elem
min	nat-even	function, nat × nat → nat
min	stut-mon	partial function, natstream × nat → nat
mkarray	array	function, nat → array
mklist	stream-of-streams	function, stream × nat → streamlist
mklist	assoclist	function, pair × nat → assoclist
mklist	string	function, char × nat → string
mklist	list-last	function, elem × nat → list
mklist	natstream	function, nat × nat → natlist
mklist	list-as-arrayinstance	function, elem × nat → array
mklist	reflist	function, Ref × nat → reflist
mkmatrix	matrix	function, nat × nat × elem → matrix
mkvector	matrixops	function, nat → vector
mon	natstream	predicate, nat → natstream
mon	mon-lim-filter-count	predicate, nat → stream
mon	streamseq-mon-lim	predicate, streamstream
mon<	stut-mon	predicate, natstream
monotone	monotone-set-fixpoint	predicate, (elem → bool) → elem → bool
mon≤	stut-mon	predicate, natstream
mx	matrixops	variable, matrix
mx	matrix	variable, matrix
mx	rowcol-upd	variable, matrix
mx	matrix+array	variable, matrix
n	list-getput	variable, nat
n	array-listops	variable, nat
n	nat-div	variable, nat
n	putoutside-id	variable, nat
n	array	variable, nat
n	list-del	variable, nat
n	olist	variable, nat
n	nat-mult	variable, nat
n	list-perm	variable, nat
n	matrixops	variable, nat
n	filter-count	variable, nat
n	intnat	variable, nat
n	nat-inf	variable, nat
n	nat-pair	variable, nat
n	array-copy	variable, nat
n	infinite-append	variable, nat
n	choice	variable, nat
n	list-data	variable, nat
n	array-revin	variable, nat
n	inf-app-list	variable, nat
n	approx-fixpoint	variable, nat
n	list-last	variable, nat
n	rowcol-upd	variable, nat
n	nat-sgn	variable, nat
n	nat-pot	variable, nat
n	mon-lim-filter-count	variable, nat
n	path-reachable	variable, nat
n	get-outside	variable, nat
n	int-pair	variable, nat
n	nat-even	variable, nat
n	natset	variable, nat
n	streamseq-mon-lim	variable, nat
n	list-set	variable, nat
n	stut-mon	variable, nat
nat	nat-basic	sort,
natinf	nat-inf	sort,
natlist	natstream	sort,
natset	natset	sort,
natstream	natstream	sort,
nextj	infinite-append	variable, nat × elem → nat
nextl	infinite-append	variable, nat × elem → list
nextli	inf-app-list	variable, list → list
nextnli	inf-app-list	variable, list × nat → list
nf	stream-basic	variable, nat → elem
nf	infinite-append	variable, nat → elem
nf	stream	variable, nat → elem
nf	choice	variable, nat → elem
nf	mon-lim-filter-count	variable, nat → elem
nfgen	infinite-append	variable, nat → nat → elem
nfgen	choice	variable, nat → nat → elem
nl	stut-mon	variable, natlist
nnf	mon-lim-filter-count	variable, nat → nat
nnf	stut-mon	variable, nat → nat
np	mon-lim-filter-count	variable, nat → bool
np	stut-mon	variable, nat → bool
ns	matrixops	variable, natset
ns	natset	variable, natset
null	Ref	constant, Ref
nσ	stut-mon	variable, natstream
n→i	intnat	function, nat → int
n∞	nat-inf	variable, natinf
n∞	mon-lim-filter-count	variable, natinf
odd	int-min	predicate, int
odd	nat-even	predicate, nat
ok	choice	predicate, elem
ordered<	olist	predicate, list
ordered<	oarray-sort	predicate, array
ordered≤	olist	predicate, list
ordered≤	oarray-sort	predicate, array
p	filter-count	variable, elem → bool
p	elem-rel	predicate, elem × elem
p	pair	variable, pair
p	mon-lim-filter-count	variable, elem → bool
p*	rtc-rel	predicate, elem × elem
p+	rtc-rel	predicate, elem × elem
pair	pair	sort,
path	path-reachable	predicate, reflist × heap
pelem	rtc-rel	variable, elem → bool
pelem	rtc	variable, elem × elem → bool
perm	list-perm	predicate, list × list
perm	list-as-arrayinstance	predicate, array × array
pos	list-del	function, elem × list → nat
pos	stream-of-streams	function, stream × streamlist → nat
pos	assoclist	function, pair × assoclist → nat
pos	string	function, char × string → nat
pos	natstream	function, nat × natlist → nat
pos	list-as-arrayinstance	function, elem × array → nat
pos	reflist	function, Ref × reflist → nat
pred	hilbert-choice	variable, elem → bool
prime	nat-prime	predicate, nat
prime	int-gcd	predicate, int
r	matrixops	variable, nat
r	matrix	variable, nat
r	rowcol-upd	variable, nat
r	path-reachable	variable, Ref
r	matrix+array	variable, nat
r	Ref	variable, Ref
reachable	path-reachable	predicate, Ref × Ref × heap
reachable*	path-reachable	predicate, heap × Ref × Ref
reachable-1	path-reachable	predicate, heap × Ref × Ref
reachable-n	path-reachable	predicate, heap × nat × Ref × Ref
reflist	reflist	sort,
rel	choice	predicate, elem × elem
rem	natstream	function, natstream × nat → bool → natstream
rem	mon-lim-filter-count	function, stream × nat → bool → stream
restn	list-del	partial function, nat × list → list
restn	stream-of-streams	partial function, nat × streamlist → streamlist
restn	assoclist	partial function, nat × assoclist → assoclist
restn	string	partial function, nat × string → string
restn	natstream	partial function, nat × natlist → natlist
restn	list-as-arrayinstance	partial function, nat × array → array
restn	reflist	partial function, nat × reflist → reflist
rev	stream-of-streams	function, streamlist → streamlist
rev	assoclist	function, assoclist → assoclist
rev	string	function, string → string
rev	array-revin	partial function, array × nat → array
rev	array-revin	function, array → array
rev	list-last	function, list → list
rev	natstream	function, natlist → natlist
rev	list-as-arrayinstance	function, array → array
rev	reflist	function, reflist → reflist
rmdup	stream-of-streams	function, streamlist → streamlist
rmdup	list-dup	function, list → list
rmdup	assoclist	function, assoclist → assoclist
rmdup	string	function, string → string
rmdup	natstream	function, natlist → natlist
rmdup	list-as-arrayinstance	function, array → array
rmdup	reflist	function, reflist → reflist
rtc	rtc-rel	predicate, nat × elem × elem
rtc	rtc	function, nat × elem × elem → bool → elem × elem → bool
s	set-basic	variable, set
s	infset-basic	variable, set
s	infset-union	variable, set
set	set-basic	sort,
set	infset-basic	sort,
sgn	int-min	function, int → int
sgn	nat-sgn	function, nat → nat
sort	oarray-sort	function, array → array
sort	olist-sort	function, list → list
sortedchars	string-less	constant, string
sqrt	int-square	partial function, int → int
st	ostore	variable, store
st	store	variable, store
st	store+set	variable, store
store	store	sort,
str	string-less	variable, string
stream	stream-basic	sort,
streamlist	stream-of-streams	sort,
streamstream	stream-of-streams	sort,
string	string	sort,
stutf	stut-mon	predicate, natstream
subarray	array-copy	partial function, array × nat × nat → array
sublist	list-del	partial function, nat × nat × list → list
sublist	stream-of-streams	partial function, nat × nat × streamlist → streamlist
sublist	assoclist	partial function, nat × nat × assoclist → assoclist
sublist	string	partial function, nat × nat × string → string
sublist	natstream	partial function, nat × nat × natlist → natlist
sublist	list-as-arrayinstance	partial function, nat × nat × array → array
sublist	reflist	partial function, nat × nat × reflist → reflist
tail	list-data	variable, list
tl	stream-of-streams	partial function, streamstream → streamstream
tl	stream	partial function, stream → stream
tl	natstream	partial function, natstream → natstream
tl	reflist	partial function, reflist → reflist
to	stream-of-streams	partial function, streamlist × nat → streamlist
to	stream-of-streams	partial function, streamstream × nat → streamstream
to	stream-of-streams	function, nat → stream × nat → streamlist
to	stream	partial function, list × nat → list
to	stream	partial function, stream × nat → stream
to	stream	function, nat → elem × nat → list
to	natstream	partial function, natlist × nat → natlist
to	natstream	partial function, natstream × nat → natstream
to	natstream	function, nat → nat × nat → natlist
to	natset	function, nat × nat → natset
toArc	rowcol-upd	function, matrix × nat → array
toArr	rowcol-upd	function, matrix × nat → array
to∞	stream-of-streams	partial function, streamstream × natinf → streamstream
to∞	stream	partial function, stream × natinf → stream
to∞	natstream	partial function, natstream × natinf → natstream
unique_al	assoclist	predicate, assoclist
vec	matrixops	variable, vector
vector	matrixops	sort,
x	list-getput	variable, list
x	putoutside-id	variable, list
x	list-del	variable, list
x	olist	variable, list
x	list-perm	variable, list
x	filter-count	variable, list
x	stream-basic	variable, list
x	list-dup	variable, list
x	list	variable, list
x	list-setequal	variable, list
x	olist-min-max	variable, list
x	stream	variable, list
x	list-data	variable, list
x	inf-app-list	variable, list
x	approx-fixpoint	variable, elem
x	list-last	variable, list
x	mon-lim-filter-count	variable, list
x	olist-sort	variable, list
x	monotone-set-fixpoint	variable, elem
x	path-reachable	variable, reflist
x	setelems	variable, elem
x	list-set	variable, list
y	list-getput	variable, list
y	list-del	variable, list
y	olist	variable, list
y	list-perm	variable, list
y	filter-count	variable, list
y	list-dup	variable, list
y	list	variable, list
y	list-setequal	variable, list
y	stream	variable, list
y	list-data	variable, list
y	inf-app-list	variable, list
y	list-last	variable, list
y	olist-sort	variable, list
y	list-set	variable, list
z	list-getput	variable, list
z	list-del	variable, list
z	olist	variable, list
z	list-perm	variable, list
z	list-dup	variable, list
z	list	variable, list
z	list-setequal	variable, list
z	stream	variable, list
z	list-data	variable, list
z	list-last	variable, list
z	olist-sort	variable, list
z	list-set	variable, list
\|	nat-prime	predicate, nat × nat
\|	int-gcd	predicate, int × int
\|	store+set	function, store × set → store
}	infset-basic	function, elem → bool → set
}	set-union	function, elem → set
}	bag-union	function, elem → bag
}	infset-union	function, elem → set
}	natset	function, nat → natset
~	int-abs	function, int → int
×	pair	function, elem × data → pair
×	int-pair	function, int × int → int
Σ	matrixops	function, natset × nat → elem → elem
ε	hilbert-choice	function, elem → bool → elem
μ	monotone-set-fixpoint	partial function, (elem → bool) → elem → bool → elem → bool
ν	monotone-set-fixpoint	partial function, (elem → bool) → elem → bool → elem → bool
σ	stream-basic	variable, stream
σ	infinite-append	variable, stream
σ	stream	variable, stream
σ	inf-app-list	variable, stream
σ	mon-lim-filter-count	variable, stream
σ	streamseq-mon-lim	variable, stream
σf	mon-lim-filter-count	variable, nat → stream
σσ	streamseq-mon-lim	variable, streamstream
χ	infset-basic	function, set → elem → bool
∅	approx-fixpoint	predicate, elem
∅	set-basic	constant, set
∅	bag-basic	constant, bag
∅	infset-basic	constant, set
∅	store	constant, store
∅	natset	constant, natset
∅	linheap	constant, heap
∈	stream-of-streams	predicate, stream × streamlist
∈	list	predicate, elem × list
∈	assoclist	predicate, elem × assoclist
∈	assoclist	predicate, pair × assoclist
∈	string	predicate, char × string
∈	array-revin	predicate, elem × array
∈	set-basic	predicate, elem × set
∈	natstream	predicate, nat × natlist
∈	infset-basic	predicate, elem × set
∈	store	predicate, elem × store
∈	list-as-arrayinstance	predicate, elem × array
∈	bag-union	predicate, elem × bag
∈	natset	predicate, nat × natset
∈	reflist	predicate, Ref × reflist
∈	linheap	predicate, Ref × heap
∈	store+set	predicate, data × store
∞	int-inf-basic	constant, intinf
∞	nat-inf	constant, natinf
∩	set-union	function, set × set → set
∩	infset-union	function, set × set → set
∩	natset	function, natset × natset → natset
∪	set-union	function, set × set → set
∪	list-as-arrayinstance	function, array × array → array
∪	bag-union	function, bag × bag → bag
∪	infset-union	function, set × set → set
∪	natset	function, natset × natset → natset
∪	list-set	function, list × list → list
∪	reflist	function, reflist × reflist → reflist
≡	list-setequal	predicate, list × list
≤	stream-of-streams	predicate, streamstream × streamstream
≤	stream	predicate, stream × stream
≤	natstream	predicate, natstream × natstream
≤	int-abs	predicate, int × int
≤	nat	predicate, nat × nat
≥	int-abs	predicate, int × int
≥	nat	predicate, nat × nat
≪	wellfounded	predicate, elem × elem
≪1	lexical-param	predicate, elem1 × elem1
≪2	lexical-param	predicate, elem2 × elem2
⊆	set-basic	predicate, set × set
⊆	infset-basic	predicate, set × set
⊆	store	predicate, store × store
⊆	list-as-arrayinstance	predicate, array × array
⊆	monotone-set-fixpoint	predicate, elem → bool × elem → bool
⊆	bag-union	predicate, bag × bag
⊆	natset	predicate, natset × natset
⊆	list-set	predicate, list × list
⊆	reflist	predicate, reflist × reflist
⊆	linheap	predicate, heap × heap
⊆m	list-perm	predicate, list × list
⊆m	list-as-arrayinstance	predicate, array × array
⊏	string	predicate, string × string
⊑	stream-of-streams	predicate, streamlist × streamlist
⊑	assoclist	predicate, assoclist × assoclist
⊑	string	predicate, string × string
⊑	list-last	predicate, list × list
⊑	natstream	predicate, natstream × natstream
⊑	natstream	predicate, natlist × natlist
⊑	mon-lim-filter-count	predicate, stream × stream
⊑	list-as-arrayinstance	predicate, array × array
⊑	streamseq-mon-lim	predicate, stream × stream
⊑	reflist	predicate, reflist × reflist
⊒	stream-of-streams	predicate, streamlist × streamlist
⊒	assoclist	predicate, assoclist × assoclist
⊒	string	predicate, string × string
⊒	list-last	predicate, list × list
⊒	natstream	predicate, natlist × natlist
⊒	list-as-arrayinstance	predicate, array × array
⊒	reflist	predicate, reflist × reflist
⊕	store+set	function, store × store → store
⌝	stream-of-streams	function, nat → stream → streamstream
⌝	stream-of-streams	function, streamlist → streamstream
⌝	int-inf-basic	function, int → intinf
⌝	nat-inf	function, nat → natinf
⌝	stream-basic	function, nat → elem → stream
⌝	stream-basic	function, list → stream
⌝	natstream	function, nat → nat → natstream
⌝	natstream	function, natlist → natstream