[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
#	natstream	function, natstream → natinf
#	natstream	function, natlist → nat
#	stream-of-streams	function, streamstream → natinf
#	stream-of-streams	function, streamlist → nat
#	bag-union	function, bag → nat
#	reflist	function, reflist → nat
#	linheap	function, heap → nat
#	stream	function, stream → natinf
#	assoclist	function, assoclist → nat
#	list-data	function, list → nat
#	array	function, array → nat
#	set-basic	function, set → nat
#	store	function, store → nat
#	string	function, string → nat
#oc	list-perm	function, elem × list → nat
%	nat-div	partial function, nat × nat → nat
%	int-div	partial function, int × int → int
'	natstream	function, nat → natlist
'	stream-of-streams	function, stream → streamlist
'	reflist	function, Ref → reflist
'	assoclist	function, pair → assoclist
'	list	function, elem → list
'	string	function, char → string
*	nat-mult	function, nat × nat → nat
*	int-mult	function, int × int → int
+	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
+	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
+	reflist	function, reflist × Ref → reflist
+	reflist	function, reflist × reflist → reflist
+	reflist	function, Ref × reflist → reflist
+	stream	function, stream × stream → stream
+	stream	function, elem × stream → stream
+	assoclist	function, assoclist × pair → assoclist
+	assoclist	function, assoclist × assoclist → assoclist
+	assoclist	function, pair × assoclist → assoclist
+	list	function, list × elem → list
+	list	function, list × list → list
+	list-data	function, elem × list → list
+	int-basic2	function, int × int → int
+	string	function, string × char → string
+	string	function, string × string → string
+	string	function, char × string → string
+	array-list	function, elem × array → array
+	nat-basic	function, nat × nat → nat
+	nat-inf	function, natinf × natinf → natinf
++	natstream	function, natlist × nat → natlist
++	stream-of-streams	function, streamlist × stream → streamlist
++	bag-basic	function, bag × elem → bag
++	reflist	function, reflist × Ref → reflist
++	infset-basic	function, set × elem → set
++	assoclist	function, assoclist × pair → assoclist
++	list-dup	function, list × elem → list
++	set-basic	function, set × elem → set
++	string	function, string × char → string
+1	int-basic1	function, int → int
+1	nat-basic	function, nat → nat
+2	reflist	function, Ref × Ref → reflist
+2	assoclist	function, pair × pair → assoclist
+2	list	function, elem × elem → list
+2	string	function, char × char → string
+l	natstream	function, nat × nat → natlist
+l	stream-of-streams	function, stream × stream → streamlist
-	int-abs	function, int × int → int
-	nat	partial function, nat × nat → nat
--	bag-union	function, bag × elem → bag
--	linheap	function, heap × Ref → heap
--	infset-union	function, set × elem → set
--	set-union	function, set × elem → set
--	store	function, store × elem → store
-1	int-basic1	function, int → int
-1	nat-basic	partial function, nat → nat
-1l	natstream	function, natlist × nat → natlist
-1l	stream-of-streams	function, streamlist × stream → streamlist
-1l	reflist	function, reflist × Ref → reflist
-1l	assoclist	function, assoclist × pair → assoclist
-1l	list-del	function, list × elem → list
-1l	string	function, string × char → string
-l	natstream	function, natlist × nat → natlist
-l	stream-of-streams	function, streamlist × stream → streamlist
-l	reflist	function, reflist × Ref → reflist
-l	assoclist	function, assoclist × pair → assoclist
-l	list-del	function, list × elem → list
-l	string	function, string × char → string
-p	stream-of-streams	function, streamlist × nat → streamlist
-p	reflist	function, reflist × nat → reflist
-p	assoclist	function, assoclist × nat → assoclist
-p	list-del	function, list × nat → list
-p	string	function, string × nat → string
-pos	natstream	function, natlist × nat → natlist
-∞	int-inf-basic	constant, intinf
.1	nat-pair	function, nat → nat
.1	int-pair	function, int → int
.1	pair	function, pair → elem
.2	nat-pair	function, nat → nat
.2	int-pair	function, int → int
.2	pair	function, pair → data
.butlast	natstream	partial function, natlist → natlist
.butlast	stream-of-streams	partial function, streamlist → streamlist
.butlast	reflist	partial function, reflist → reflist
.butlast	assoclist	partial function, assoclist → assoclist
.butlast	list-last	partial function, list → list
.butlast	string	partial function, string → string
.butmax	oset	partial function, set → set
.butmin	ostore	partial function, store → store
.butmin	oset	partial function, set → set
.char1	string	partial function, string → char
.f	natstream	partial function, natstream → nat → nat
.f	stream-of-streams	partial function, streamstream → nat → stream
.f	stream-basic	partial function, stream → nat → elem
.first	array-list	partial function, array → elem
.head	natstream	partial function, natlist → nat
.head	stream-of-streams	partial function, streamlist → stream
.head	assoclist	partial function, assoclist → pair
.head	list-data	partial function, list → elem
.i	int-inf-basic	partial function, intinf → int
.keys	ostore	function, store → set
.l	natstream	partial function, natstream → natlist
.l	stream-of-streams	partial function, streamstream → streamlist
.l	stream-basic	partial function, stream → list
.last	natstream	partial function, natlist → nat
.last	stream-of-streams	partial function, streamlist → stream
.last	reflist	partial function, reflist → Ref
.last	assoclist	partial function, assoclist → pair
.last	list-last	partial function, list → elem
.last	string	partial function, string → char
.map	store-map	function, store × elem × data → data → store
.map	store-map	function, store × data → data → store
.max	oset	partial function, set → elem
.min	ostore	partial function, store → elem
.min	oset	partial function, set → elem
.n	nat-inf	partial function, natinf → nat
.nxt	lincell	function, cell → Ref
.rest	array-list	partial function, array → array
.rstring	string	partial function, string → string
.tail	natstream	partial function, natlist → natlist
.tail	stream-of-streams	partial function, streamlist → streamlist
.tail	assoclist	partial function, assoclist → assoclist
.tail	list-data	partial function, list → list
/	nat-div	partial function, nat × nat → nat
/	int-div	partial function, int × int → int
2^	nat-pot	function, nat → nat
<	natstream	predicate, natlist × natlist
<	stream-of-streams	predicate, streamlist × streamlist
<	reflist	predicate, reflist × reflist
<	int-inf	predicate, intinf × intinf
<	assoclist	predicate, assoclist × assoclist
<	oset	predicate, set × elem
<	oset	predicate, elem × set
<	list-data	predicate, list × list
<	int-basic1	predicate, int × int
<	oelem	predicate, elem × elem
<	string-less	predicate, char × char
<	string-less	predicate, string × string
<	array-list	predicate, array × array
<	nat-basic	predicate, nat × nat
<	nat-inf	predicate, natinf × natinf
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
A	wellfounded-TL	variable, elem,flexible
H	linheap	variable, heap
H0	linheap	variable, heap
H1	linheap	variable, heap
H2	linheap	variable, heap
IHP	wellfounded	variable, elem → bool
IHP	lexical-param	variable, elem1 → bool
IHPQ	lexical	variable, elem1 × elem2 → bool
IHQ	lexical-param	variable, elem2 → bool
IS	monotone-set-fixpoint	function, (elem → bool) → bool → elem → bool
N	wellfounded-TL	variable, nat,flexible
P	hilbert-choice	variable, elem → bool
Pelem	rtc-rel	variable, elem → bool
Pelem	rtc	variable, elem × elem → bool
Ref	Ref	sort,
S	monotone-set-fixpoint	variable, elem → bool
S0	monotone-set-fixpoint	variable, elem → bool
S1	monotone-set-fixpoint	variable, elem → bool
SS	monotone-set-fixpoint	variable, (elem → bool) → bool
Sn	approx-fixpoint	variable, nat → elem → bool
UN	monotone-set-fixpoint	function, (elem → bool) → bool → elem → bool
[]	natstream	constant, natstream
[]	natstream	constant, natlist
[]	stream-of-streams	constant, streamstream
[]	stream-of-streams	constant, streamlist
[]	reflist	constant, reflist
[]	stream	constant, stream
[]	assoclist	constant, assoclist
[]	list-data	constant, list
[]	array-list	constant, array
\	store+set	function, store × set → store
\	bag-union	function, bag × bag → bag
\	reflist	function, reflist × reflist → reflist
\	infset-union	function, set × set → set
\	list-set	function, list × list → list
\	set-union	function, set × set → set
]	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
]	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
]	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
]	stream	partial function, stream × nat × elem → stream
]	stream	partial function, stream × 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
]	list-del	partial function, list × nat × elem → list
]	list-del	partial function, list × nat → elem
]	array	partial function, array × nat × elem → array
]	array	partial function, array × nat → elem
]	store	partial function, store × elem → data
]	store	function, store × elem × data → store
]	string	partial function, string × nat × char → string
]	string	partial function, string × nat → char
^	approx-fixpoint	function, (elem → bool) → elem → bool × nat → (elem → bool) → elem → bool
^	int-pot	partial function, int × int → int
^	nat-pot	function, nat × nat → nat
^*	rtc	function, elem × elem → bool → elem × elem → bool
^2	int-square	function, int → int
a	hilbert-choice	variable, elem
a	elem	variable, elem
a	wellfounded	variable, elem
a	lexical-param	variable, elem1
a0	list-data	variable, elem
a0	pair	variable, elem
a0	wellfounded	variable, elem
a0	lexical-param	variable, elem1
a1	wellfounded	variable, elem
a1	lexical-param	variable, elem1
aa	choice	constant, elem
abs	int-abs	function, int → int
ar	array	variable, array
ar0	array	variable, array
ar1	array	variable, array
ar10	array-list	variable, array
ar2	array	variable, array
ar3	array-list	variable, array
ar4	array-list	variable, array
ar5	array-list	variable, array
ar6	array-list	variable, array
ar7	array-list	variable, array
ar8	array-list	variable, array
ar9	array-list	variable, array
array	array	sort,
assoclist	assoclist	sort,
ax	assoclist	variable, assoclist
ax0	assoclist	variable, assoclist
ax1	assoclist	variable, assoclist
ay	assoclist	variable, assoclist
az	assoclist	variable, assoclist
b	elem	variable, elem
b	lexical-param	variable, elem2
b0	lexical-param	variable, elem2
b1	lexical-param	variable, elem2
bag	bag-basic	variable, bag
bag	bag-basic	sort,
bag0	bag-basic	variable, bag
bag1	bag-basic	variable, bag
bag2	bag-basic	variable, bag
bool	bool	sort,
boolvar	bool	variable, bool
boolvar0	bool	variable, bool
butlastn	natstream	partial function, nat × natlist → natlist
butlastn	stream-of-streams	partial function, nat × streamlist → streamlist
butlastn	reflist	partial function, nat × reflist → reflist
butlastn	assoclist	partial function, nat × assoclist → assoclist
butlastn	list-last	partial function, nat × list → list
butlastn	string	partial function, nat × string → string
c	elem	variable, elem
ce	lincell	variable, cell
ce0	linheap	variable, cell
ce1	linheap	variable, cell
ce2	linheap	variable, cell
cell	lincell	sort,
chain	approx-fixpoint	predicate, nat → elem → bool
char	char	variable, char
char	char	sort,
char0	char	variable, char
char1	char	variable, char
char2	char	variable, char
char3	string-less	variable, char
cmp	array-copy	partial predicate, array × elem × nat × nat
cmp	array-copy	partial predicate, array × nat × array × nat × nat
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	bag-basic	function, elem × bag → nat
d	data	variable, data
d0	data	variable, data
d1	data	variable, data
d2	data	variable, data
data	data	sort,
dataf	store-map	variable, data → data
decode	int-pair	function, int → nat
decode	int-pair	function, nat → int
disj	natstream	predicate, natlist × natlist
disj	stream-of-streams	predicate, streamlist × streamlist
disj	reflist	predicate, reflist × reflist
disj	assoclist	predicate, assoclist × assoclist
disj	list-dup	predicate, list × list
disj	string	predicate, string × string
dist	nat-prime	function, nat × nat → nat
dom	store+set	function, store → set
dups	natstream	predicate, natlist
dups	stream-of-streams	predicate, streamlist
dups	reflist	predicate, reflist
dups	assoclist	predicate, assoclist
dups	list-dup	predicate, list
dups	string	predicate, string
elem	setelems	sort,
elem	hilbert-choice	sort,
elem	elem	sort,
elem	wellfounded	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	monotone-set-fixpoint	variable, (elem → bool) → elem → bool
f	characteristic	variable, elem → bool
fill	array-copy	partial function, array × elem × nat × nat → array
fill	array-copy	function, array × elem → array
fillfirst	natstream	function, nat × nat × natlist → natlist
fillfirst	stream-of-streams	function, nat × stream × streamlist → streamlist
fillfirst	reflist	function, nat × Ref × reflist → reflist
fillfirst	assoclist	function, nat × pair × assoclist → assoclist
fillfirst	list-last	function, nat × elem × list → list
fillfirst	string	function, nat × char × string → string
filter	natstream	function, nat → bool × natstream → natstream
filter	mon-lim-filter-count	function, elem → bool × stream → stream
filter	reflist	function, reflist × reflist → reflist
filter	list-set	function, list × list → list
finp	natstream	predicate, natstream
finp	stream-of-streams	predicate, streamstream
finp	stream-basic	predicate, stream
firstn	natstream	partial function, nat × natlist → natlist
firstn	stream-of-streams	partial function, nat × streamlist → streamlist
firstn	reflist	partial function, nat × reflist → reflist
firstn	assoclist	partial function, nat × assoclist → assoclist
firstn	list-del	partial function, nat × list → list
firstn	string	partial function, nat × string → string
from	natstream	partial function, natlist × nat → natlist
from	natstream	partial function, natstream × nat → natstream
from	natstream	function, nat → nat × nat → nat → nat
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
frome	natstream	function, natlist × nat → natlist
frome	stream-of-streams	function, streamlist × stream → streamlist
frome	reflist	function, reflist × Ref → reflist
frome	assoclist	function, assoclist × pair → assoclist
frome	list-del	function, list × elem → list
frome	string	function, string × char → string
gcd	int-gcd	function, int × int → int
gcd	nat-prime	function, nat × nat → nat
hd	natstream	partial function, natstream → nat
hd	stream-of-streams	partial function, streamstream → stream
hd	reflist	partial function, reflist → Ref
hd	stream	partial function, stream → elem
heap	linheap	sort,
i	int-basic1	variable, int
i0	int-basic1	variable, int
idrange	array-copy	partial predicate, array × nat × nat
id○	array-copy	predicate, array × array × nat
ii	infinite-append	variable, nat → nat
iigen	infinite-append	variable, nat → nat → nat
ins≤	olist	function, elem × list → list
int	int-basic1	sort,
intinf	int-inf-basic	sort,
inv	stut-mon	partial function, natstream → natstream
inv	rtc-rel	predicate, elem × elem → bool
i→n	intnat	function, int → nat
i∞	int-inf-basic	variable, intinf
j	int-basic1	variable, int
j0	int-basic1	variable, int
jj	infinite-append	variable, nat → nat
lastn	natstream	partial function, nat × natlist → natlist
lastn	stream-of-streams	partial function, nat × streamlist → streamlist
lastn	reflist	partial function, nat × reflist → reflist
lastn	assoclist	partial function, nat × assoclist → assoclist
lastn	list-del	partial function, nat × list → list
lastn	string	partial function, nat × string → string
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
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	nat-basic	variable, nat
m0	nat-pot	variable, nat
m0	array-copy	variable, nat
m0	nat-inf	variable, nat
m1	natstream	variable, nat
m2	natstream	variable, nat
m3	natstream	variable, nat
m4	natstream	variable, nat
max	olist-min-max	partial function, list → elem
max	oelem-min-max	function, elem × elem → elem
max	int-min	function, int × int → int
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
min	olist-min-max	partial function, list → elem
min	oelem-min-max	function, elem × elem → elem
min	stut-mon	partial function, natstream × nat → nat
min	int-min	function, int × int → int
min	nat-even	function, nat × nat → nat
min	nat-inf	function, natinf × natinf → natinf
mkarray	array	function, nat → array
mklist	natstream	function, nat × nat → natlist
mklist	stream-of-streams	function, stream × nat → streamlist
mklist	reflist	function, Ref × nat → reflist
mklist	assoclist	function, pair × nat → assoclist
mklist	list-last	function, elem × nat → list
mklist	string	function, char × nat → string
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
n	nat-basic	variable, nat
n0	nat-basic	variable, nat
n1	nat-basic	variable, nat
nat	nat-basic	sort,
natinf	nat-inf	sort,
natlist	natstream	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	choice	variable, nat → elem
nf	stream-basic	variable, nat → elem
nf0	stream-basic	variable, nat → elem
nfgen	choice	variable, nat → nat → elem
nfgen	infinite-append	variable, nat → nat → elem
nl	natstream	variable, natlist
nl0	natstream	variable, natlist
nl1	natstream	variable, natlist
nl2	natstream	variable, natlist
nl5	natstream	variable, natlist
nnf	mon-lim-filter-count	variable, nat → nat
nnf0	natstream	variable, nat → nat
nnf1	natstream	variable, nat → nat
np	mon-lim-filter-count	variable, nat → bool
np0	natstream	variable, nat → bool
null	Ref	constant, Ref
nσ	natstream	variable, natstream
nσ0	natstream	variable, natstream
nσ1	natstream	variable, natstream
nσ2	natstream	variable, natstream
nσf	natstream	variable, nat → natstream
n→i	intnat	function, nat → int
n∞	nat-inf	variable, natinf
n∞0	nat-inf	variable, natinf
odd	int-min	predicate, int
odd	nat-even	predicate, nat
ok	choice	predicate, elem
ordered<	olist	predicate, list
ordered≤	olist	predicate, list
p	mon-lim-filter-count	variable, elem → bool
p	elem-rel	predicate, elem × elem
p	pair	variable, pair
p*	rtc-rel	predicate, elem × elem
p+	rtc-rel	predicate, elem × elem
p0	pair	variable, pair
p1	pair	variable, pair
p2	pair	variable, pair
pair	pair	sort,
path	path-reachable	predicate, reflist × heap
perm	list-perm	predicate, list × list
pos	natstream	function, nat × natlist → nat
pos	stream-of-streams	function, stream × streamlist → nat
pos	reflist	function, Ref × reflist → nat
pos	assoclist	function, pair × assoclist → nat
pos	list-del	function, elem × list → nat
pos	string	function, char × string → nat
prime	int-gcd	predicate, int
prime	nat-prime	predicate, nat
r	Ref	variable, Ref
r0	reflist	variable, Ref
r0	linheap	variable, Ref
r1	reflist	variable, Ref
r1	linheap	variable, Ref
r2	reflist	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	natstream	partial function, nat × natlist → natlist
restn	stream-of-streams	partial function, nat × streamlist → streamlist
restn	reflist	partial function, nat × reflist → reflist
restn	assoclist	partial function, nat × assoclist → assoclist
restn	list-del	partial function, nat × list → list
restn	string	partial function, nat × string → string
rev	natstream	function, natlist → natlist
rev	stream-of-streams	function, streamlist → streamlist
rev	reflist	function, reflist → reflist
rev	assoclist	function, assoclist → assoclist
rev	list-last	function, list → list
rev	array-copy	partial function, array × nat → array
rev	array-copy	function, array → array
rev	string	function, string → string
rmdup	natstream	function, natlist → natlist
rmdup	stream-of-streams	function, streamlist → streamlist
rmdup	reflist	function, reflist → reflist
rmdup	assoclist	function, assoclist → assoclist
rmdup	list-dup	function, list → list
rmdup	string	function, string → string
rtc	rtc-rel	predicate, nat × elem × elem
rtc	rtc	function, nat × elem × elem → bool → elem × elem → bool
s	infset-basic	variable, set
s	set-basic	variable, set
s0	infset-basic	variable, set
s0	set-basic	variable, set
s1	infset-basic	variable, set
s1	set-basic	variable, set
s2	infset-basic	variable, set
s2	set-basic	variable, set
set	infset-basic	sort,
set	set-basic	sort,
sgn	nat-sgn	function, nat → nat
sgn	int-min	function, int → int
sort	olist-sort	function, list → list
sortedchars	string-less	constant, string
sqrt	int-square	partial function, int → int
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
store	store	sort,
str	string	variable, string
str0	string	variable, string
str1	string	variable, string
str2	string	variable, string
str3	string	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	natstream	partial function, nat × nat × natlist → natlist
sublist	stream-of-streams	partial function, nat × nat × streamlist → streamlist
sublist	reflist	partial function, nat × nat × reflist → reflist
sublist	assoclist	partial function, nat × nat × assoclist → assoclist
sublist	list-del	partial function, nat × nat × list → list
sublist	string	partial function, nat × nat × string → string
tl	natstream	partial function, natstream → natstream
tl	stream-of-streams	partial function, streamstream → streamstream
tl	reflist	partial function, reflist → reflist
tl	stream	partial function, stream → stream
to	natstream	partial function, natlist × nat → natlist
to	natstream	partial function, natstream × nat → natstream
to	natstream	function, nat → nat × nat → natlist
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, natstream × natinf → natstream
to∞	stream-of-streams	partial function, streamstream × natinf → streamstream
to∞	stream	partial function, stream × natinf → stream
unique_al	assoclist	predicate, assoclist
x	setelems	variable, elem
x	reflist	variable, reflist
x	list-data	variable, list
x0	monotone-set-fixpoint	variable, elem
x0	reflist	variable, reflist
x0	list-data	variable, list
x1	monotone-set-fixpoint	variable, elem
x1	reflist	variable, reflist
x1	list-data	variable, list
y	reflist	variable, reflist
y	list-data	variable, list
z	reflist	variable, reflist
z	list-data	variable, list
\|	store+set	function, store × set → store
\|	int-gcd	predicate, int × int
\|	nat-prime	predicate, nat × nat
}	bag-union	function, elem → bag
}	characteristic	function, elem → bool → set
}	infset-union	function, elem → set
}	set-union	function, elem → set
~	int-abs	function, int → int
×	int-pair	function, int × int → int
×	pair	function, elem × data → pair
ε	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
σ0	mon-lim-filter-count	variable, stream
σ0	stream-of-streams	variable, stream
σ1	stream	variable, stream
σ2	stream	variable, stream
σf	mon-lim-filter-count	variable, nat → stream
σf	stream-of-streams	variable, nat → stream
σf0	stream-of-streams	variable, nat → stream
σx	stream-of-streams	variable, streamlist
σx0	stream-of-streams	variable, streamlist
σx1	stream-of-streams	variable, streamlist
σy	stream-of-streams	variable, streamlist
σz	stream-of-streams	variable, streamlist
σσ	stream-of-streams	variable, streamstream
σσ1	stream-of-streams	variable, streamstream
σσ2	stream-of-streams	variable, streamstream
χ	characteristic	function, set → elem → bool
∅	bag-basic	constant, bag
∅	linheap	constant, heap
∅	infset-basic	constant, set
∅	set-basic	constant, set
∅	store	constant, store
∈	natstream	predicate, nat × natlist
∈	stream-of-streams	predicate, stream × streamlist
∈	store+set	predicate, data × store
∈	bag-union	predicate, elem × bag
∈	reflist	predicate, Ref × reflist
∈	linheap	predicate, Ref × heap
∈	infset-basic	predicate, elem × set
∈	assoclist	predicate, elem × assoclist
∈	assoclist	predicate, pair × assoclist
∈	list	predicate, elem × list
∈	array-copy	predicate, elem × array
∈	set-basic	predicate, elem × set
∈	store	predicate, elem × store
∈	string	predicate, char × string
∞	int-inf-basic	constant, intinf
∞	nat-inf	constant, natinf
∩	infset-union	function, set × set → set
∩	set-union	function, set × set → set
∪	bag-union	function, bag × bag → bag
∪	reflist	function, reflist × reflist → reflist
∪	infset-union	function, set × set → set
∪	list-set	function, list × list → list
∪	set-union	function, set × set → set
≡	list-setequal	predicate, list × list
≤	natstream	predicate, natstream × natstream
≤	stream-of-streams	predicate, streamstream × streamstream
≤	stream	predicate, stream × stream
≤	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
⊆	monotone-set-fixpoint	predicate, elem → bool × elem → bool
⊆	bag-union	predicate, bag × bag
⊆	reflist	predicate, reflist × reflist
⊆	linheap	predicate, heap × heap
⊆	infset-basic	predicate, set × set
⊆	list-set	predicate, list × list
⊆	set-basic	predicate, set × set
⊆	store	predicate, store × store
⊆m	list-perm	predicate, list × list
⊏	string	predicate, string × string
⊑	natstream	predicate, natstream × natstream
⊑	natstream	predicate, natlist × natlist
⊑	mon-lim-filter-count	predicate, stream × stream
⊑	stream-of-streams	predicate, streamlist × streamlist
⊑	streamseq-mon-lim	predicate, stream × stream
⊑	reflist	predicate, reflist × reflist
⊑	assoclist	predicate, assoclist × assoclist
⊑	list-last	predicate, list × list
⊑	string	predicate, string × string
⊒	natstream	predicate, natlist × natlist
⊒	stream-of-streams	predicate, streamlist × streamlist
⊒	reflist	predicate, reflist × reflist
⊒	assoclist	predicate, assoclist × assoclist
⊒	list-last	predicate, list × list
⊒	string	predicate, string × string
⊕	store+set	function, store × store → store
⌝	natstream	function, nat → nat → natstream
⌝	natstream	function, natlist → natstream
⌝	stream-of-streams	function, nat → stream → streamstream
⌝	stream-of-streams	function, streamlist → streamstream
⌝	int-inf-basic	function, int → intinf
⌝	stream-basic	function, nat → elem → stream
⌝	stream-basic	function, list → stream
⌝	nat-inf	function, nat → natinf