[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
#	string-less	function, string → nat
#	assoclista	function, assoclist → nat
#	list-data	function, list → nat
#	array	function, array → nat
#	set-basic	function, set → nat
#	store	function, store → nat
#	string-new	function, string → nat
#oc	list-perm	function, elem × list → nat
%	nat-div	function, nat × nat → nat
%	int-div	function, int × int → int
'	natstream	function, nat → natlist
'	stream-of-streams	function, stream → streamlist
'	reflist	function, Ref → reflist
'	assoclista	function, pair → assoclist
'	list	function, elem → list
'	string-append	function, char → string
'	string-new	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, Ref × Ref → reflist
+	reflist	function, reflist × Ref → reflist
+	reflist	function, reflist × reflist → reflist
+	reflist	function, Ref × reflist → reflist
+	nat-inf	function, natinf × natinf → natinf
+	stream	function, stream × stream → stream
+	stream	function, elem × stream → stream
+	assoclista	function, pair × pair → assoclist
+	assoclista	function, assoclist × pair → assoclist
+	assoclista	function, assoclist × assoclist → assoclist
+	assoclista	function, pair × assoclist → assoclist
+	list	function, elem × elem → list
+	list	function, list × elem → list
+	list	function, list × list → list
+	list-data	function, elem × list → list
+	string-append	function, string × string → string
+	string-data	function, char × string → string
+	int-basic2	function, int × int → int
+	nat-basic2	function, nat × nat → nat
+	string-new	function, char × char → string
+	string-new	function, string × char → string
+	string-new	function, string × string → string
+	string-new	function, char × string → string
+	array-list	function, elem × array → array
++	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
++	assoclista	function, assoclist × pair → assoclist
++	list-dup	function, list × elem → list
++	set-basic	function, set × elem → set
++	string-new	function, string × char → string
+1	int-basic1	function, int → int
+1	nat-basic1	function, nat → nat
+l	natstream	function, nat × nat → natlist
+l	stream-of-streams	function, stream × stream → streamlist
-	int-abs	function, int × int → int
-	nat	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-basic1	function, nat → nat
-1l	natstream	function, natlist × nat → natlist
-1l	stream-of-streams	function, streamlist × nat → streamlist
-1l	stream-of-streams	function, streamlist × stream → streamlist
-1l	reflist	function, reflist × nat → reflist
-1l	reflist	function, reflist × Ref → reflist
-1l	assoclista	function, assoclist × nat → assoclist
-1l	assoclista	function, assoclist × pair → assoclist
-1l	list-del	function, list × nat → list
-1l	list-del	function, list × elem → list
-1l	string-new	function, string × nat → string
-1l	string-new	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	assoclista	function, assoclist × pair → assoclist
-l	list-del	function, list × elem → list
-l	string-new	function, string × char → 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	function, natlist → natlist
.butlast	stream-of-streams	function, streamlist → streamlist
.butlast	reflist	function, reflist → reflist
.butlast	assoclista	function, assoclist → assoclist
.butlast	list-last	function, list → list
.butlast	string-new	function, string → string
.butmax	oset	function, set → set
.butmin	ostore	function, store → store
.butmin	oset	function, set → set
.char1	string-data	function, string → char
.char1	string-new	function, string → char
.f	natstream	function, natstream → nat → nat
.f	stream-of-streams	function, streamstream → nat → stream
.f	stream-basic	function, stream → nat → elem
.first	natstream	function, natlist → nat
.first	stream-of-streams	function, streamlist → stream
.first	assoclista	function, assoclist → pair
.first	list-data	function, list → elem
.first	array-list	function, array → elem
.i	int-inf-basic	function, intinf → int
.keys	ostore	function, store → set
.l	natstream	function, natstream → natlist
.l	stream-of-streams	function, streamstream → streamlist
.l	stream-basic	function, stream → list
.last	natstream	function, natlist → nat
.last	stream-of-streams	function, streamlist → stream
.last	reflist	function, reflist → Ref
.last	assoclista	function, assoclist → pair
.last	list-last	function, list → elem
.last	string-new	function, string → char
.map	store-map	function, store × elem × data → data → store
.map	store-map	function, store × data → data → store
.max	oset	function, set → elem
.min	ostore	function, store → elem
.min	oset	function, set → elem
.n	nat-inf-basic	function, natinf → nat
.nxt	lincell	function, cell → Ref
.rest	natstream	function, natlist → natlist
.rest	stream-of-streams	function, streamlist → streamlist
.rest	assoclista	function, assoclist → assoclist
.rest	list-data	function, list → list
.rest	array-list	function, array → array
.rstring	string-data	function, string → string
.rstring	string-new	function, string → string
/	nat-div	function, nat × nat → nat
/	int-div	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
<	nat-inf	predicate, natinf × natinf
<	string-less	predicate, char × char
<	string-less	predicate, string × string
<	assoclista	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
<	nat-basic1	predicate, nat × nat
<	string-less-new	predicate, char × char
<	string-less-new	predicate, string × string
<	array-list	predicate, array × array
>	int-abs	predicate, int × int
>	nat	predicate, nat × nat
Boolvar	compat-store	variable, bool,flexible
H	linheap	variable, heap
H0	linheap	variable, heap
H1	linheap	variable, heap
H2	linheap	variable, heap
IS	monotone-set-fixpoint	function, (elem → bool) → bool → elem → bool
P	hilbert-choice	variable, elem → bool
Pelem	rtc-rel	variable, elem → bool
Pelem	rtc	variable, elem × elem → bool
Pstore	compat-store	variable, store → 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
[]	assoclista	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	function, natstream × nat × nat → natstream
]	natstream	function, natstream × nat → nat
]	natstream	function, natlist × nat × nat → natlist
]	natstream	function, natlist × nat → nat
]	stream-of-streams	function, streamstream × nat × stream → streamstream
]	stream-of-streams	function, streamstream × nat → stream
]	stream-of-streams	function, streamlist × nat × stream → streamlist
]	stream-of-streams	function, streamlist × nat → stream
]	reflist	function, reflist × nat × Ref → reflist
]	reflist	function, reflist × nat → Ref
]	linheap	function, heap × Ref → cell
]	linheap	function, heap × Ref × cell → heap
]	stream	function, stream × nat × elem → stream
]	stream	function, stream × nat → elem
]	assoclist	function, assoclist × elem × data → assoclist
]	assoclist	function, assoclist × data → elem
]	assoclist	function, assoclist × elem → data
]	assoclista	function, assoclist × nat × pair → assoclist
]	assoclista	function, assoclist × nat → pair
]	list-del	function, list × nat × elem → list
]	list-del	function, list × nat → elem
]	array	function, array × nat × elem → array
]	array	function, array × nat → elem
]	store	function, store × elem → data
]	store	function, store × elem × data → store
]	string-new	function, string × nat × char → string
]	string-new	function, string × nat → char
^	approx-fixpoint	function, (elem → bool) → elem → bool × nat → (elem → bool) → elem → bool
^	int-pot	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
a0	list-data	variable, elem
a0	store	variable, elem
a0	pair	variable, elem
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	assoclista	sort,
ax	assoclista	variable, assoclist
ax0	assoclista	variable, assoclist
ax1	assoclista	variable, assoclist
ax2	assoclista	variable, assoclist
ay	assoclista	variable, assoclist
ay0	assoclista	variable, assoclist
ay1	assoclista	variable, assoclist
ay2	assoclista	variable, assoclist
az	assoclista	variable, assoclist
az0	assoclista	variable, assoclist
az1	assoclista	variable, assoclist
az2	assoclista	variable, assoclist
b	elem	variable, elem
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	compat-store	variable, bool
boolvar	bool	variable, bool
boolvar0	compat-store	variable, bool
boolvar0	bool	variable, bool
boolvar1	compat-store	variable, bool
butlastn	natstream	function, nat × natlist → natlist
butlastn	stream-of-streams	function, nat × streamlist → streamlist
butlastn	reflist	function, nat × reflist → reflist
butlastn	assoclista	function, nat × assoclist → assoclist
butlastn	list-last	function, nat × list → list
butlastn	string-new	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
char3	string-less-new	variable, char
cmp	array-copy	predicate, array × elem × nat × nat
cmp	array-copy	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	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	assoclista	predicate, assoclist × assoclist
disj	list-dup	predicate, list × list
disj	string-new	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	assoclista	predicate, assoclist
dups	list-dup	predicate, list
dups	string-new	predicate, string
elem	setelems	sort,
elem	hilbert-choice	sort,
elem	elem	sort,
elemdata	store	sort,
elemdataf	store-map	variable, elem × data → data
elemdatavar	store	variable, elemdata
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	function, array × elem → array
fill	array-copy	function, array × elem × nat × nat → 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	assoclista	function, nat × pair × assoclist → assoclist
fillfirst	list-last	function, nat × elem × list → list
fillfirst	string-new	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	function, nat × natlist → natlist
firstn	stream-of-streams	function, nat × streamlist → streamlist
firstn	reflist	function, nat × reflist → reflist
firstn	assoclista	function, nat × assoclist → assoclist
firstn	list-del	function, nat × list → list
firstn	string-new	function, nat × string → string
from	natstream	function, nat → nat × nat → nat → nat
from	natstream	function, natlist × nat → natlist
from	natstream	function, natstream × nat → natstream
from	stream-of-streams	function, nat → stream × nat → nat → stream
from	stream-of-streams	function, streamlist × nat → streamlist
from	stream-of-streams	function, streamstream × nat → streamstream
from	stream	function, nat → elem × nat → nat → elem
from	stream	function, list × nat → list
from	stream	function, stream × nat → stream
frome	natstream	function, natlist × nat → natlist
frome	stream-of-streams	function, streamlist × stream → streamlist
frome	reflist	function, reflist × Ref → reflist
frome	assoclista	function, assoclist × pair → assoclist
frome	list-del	function, list × elem → list
frome	string-new	function, string × char → string
gcd	int-gcd	function, int × int → int
gcd	nat-prime	function, nat × nat → nat
hd	natstream	function, natstream → nat
hd	stream-of-streams	function, streamstream → stream
hd	reflist	function, reflist → Ref
hd	stream	function, stream → elem
heap	linheap	sort,
i	int-basic1	variable, int
i0	int-basic1	variable, int
idrange	array-copy	predicate, array × nat × nat
id○	array-copy	predicate, array × array × nat
ii	infinite-append	variable, nat → nat
iigen	infinite-append	variable, nat → nat → nat
insert	lookup	function, elem × data × store → store
ins≤	olist	function, elem × list → list
int	int-basic1	sort,
intinf	int-inf-basic	sort,
inv	stut-mon	function, natstream → natstream
inv	rtc-rel	predicate, elem × elem → bool
isSquare	int-square	predicate, int
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	function, nat × natlist → natlist
lastn	stream-of-streams	function, nat × streamlist → streamlist
lastn	reflist	function, nat × reflist → reflist
lastn	assoclista	function, nat × assoclist → assoclist
lastn	list-del	function, nat × list → list
lastn	string-new	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
lf	infinite-append	variable, nat → list
lfgen	infinite-append	variable, nat → nat → list
lim	natstream	function, nat → natstream → natstream
lim	mon-lim-filter-count	function, nat → stream → stream
lim	streamseq-mon-lim	function, streamstream → stream
list	list-data	sort,
log	nat-pot	function, nat × nat → nat
log2	nat-pot	function, nat → nat
lookup	lookup	function, elem × store → data
m	nat-basic1	variable, nat
m0	nat-inf-basic	variable, nat
m0	array-copy	variable, nat
m1	natstream	variable, nat
m2	natstream	variable, nat
m3	natstream	variable, nat
m4	natstream	variable, nat
max	olist-min-max	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	function, list → elem
min	oelem-min-max	function, elem × elem → elem
min	stut-mon	function, natstream × nat → nat
min	nat-inf	function, natinf × natinf → natinf
min	int-min	function, int × int → int
min	nat-even	function, nat × nat → nat
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	assoclista	function, pair × nat → assoclist
mklist	list-last	function, elem × nat → list
mklist	string-new	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-basic1	variable, nat
n0	nat-basic1	variable, nat
n1	nat-basic1	variable, nat
nat	nat-basic1	sort,
natinf	nat-inf-basic	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
nl10	natstream	variable, natlist
nl2	natstream	variable, natlist
nl3	natstream	variable, natlist
nl4	natstream	variable, natlist
nl5	natstream	variable, natlist
nl6	natstream	variable, natlist
nl7	natstream	variable, natlist
nl8	natstream	variable, natlist
nl9	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-basic	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	string-less	function, char × string → nat
pos	assoclista	function, pair × assoclist → nat
pos	list-del	function, elem × list → nat
pos	string-new	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
r2	linheap	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	function, nat × natlist → natlist
restn	stream-of-streams	function, nat × streamlist → streamlist
restn	reflist	function, nat × reflist → reflist
restn	assoclista	function, nat × assoclist → assoclist
restn	list-del	function, nat × list → list
restn	string-new	function, nat × string → string
rev	natstream	function, natlist → natlist
rev	stream-of-streams	function, streamlist → streamlist
rev	reflist	function, reflist → reflist
rev	assoclista	function, assoclist → assoclist
rev	list-last	function, list → list
rev	array-copy	function, array × nat → array
rev	array-copy	function, array → array
rev	string-new	function, string → string
rinv	stut-mon	function, natstream → nat → nat
rmdup	natstream	function, natlist → natlist
rmdup	stream-of-streams	function, streamlist → streamlist
rmdup	reflist	function, reflist → reflist
rmdup	assoclista	function, assoclist → assoclist
rmdup	list-dup	function, list → list
rmdup	string-new	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
sortedchars	string-less-new	constant, string
sqrt	int-square	function, int → int
st	store	variable, store
st0	store	variable, store
st1	store	variable, store
st2	store	variable, store
store	store	sort,
str	string-data	variable, string
str	string-new	variable, string
str0	string-data	variable, string
str0	string-new	variable, string
str1	string-data	variable, string
str1	string-new	variable, string
str10	string-new	variable, string
str2	string-data	variable, string
str2	string-new	variable, string
str3	string-data	variable, string
str3	string-new	variable, string
str4	string-new	variable, string
str5	string-new	variable, string
str6	string-new	variable, string
str7	string-new	variable, string
str8	string-new	variable, string
str9	string-new	variable, string
stream	stream-basic	sort,
streamlist	stream-of-streams	sort,
streamstream	stream-of-streams	sort,
string	string-data	sort,
string	string-new	sort,
stringvar	string-append	variable, string
stringvar0	string-append	variable, string
stutf	stut-mon	predicate, natstream
subarray	array-copy	function, array × nat × nat → array
sublist	natstream	function, nat × nat × natlist → natlist
sublist	stream-of-streams	function, nat × nat × streamlist → streamlist
sublist	reflist	function, nat × nat × reflist → reflist
sublist	assoclista	function, nat × nat × assoclist → assoclist
sublist	list-del	function, nat × nat × list → list
sublist	string-new	function, nat × nat × string → string
tl	natstream	function, natstream → natstream
tl	stream-of-streams	function, streamstream → streamstream
tl	reflist	function, reflist → reflist
tl	stream	function, stream → stream
to	natstream	function, nat → nat × nat → natlist
to	natstream	function, natlist × nat → natlist
to	natstream	function, natstream × nat → natstream
to	stream-of-streams	function, nat → stream × nat → streamlist
to	stream-of-streams	function, streamlist × nat → streamlist
to	stream-of-streams	function, streamstream × nat → streamstream
to	stream	function, nat → elem × nat → list
to	stream	function, list × nat → list
to	stream	function, stream × nat → stream
to∞	natstream	function, natstream × natinf → natstream
to∞	stream-of-streams	function, streamstream × natinf → streamstream
to∞	stream	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
x2	reflist	variable, reflist
x2	list-data	variable, list
y	reflist	variable, reflist
y	list-data	variable, list
y0	reflist	variable, reflist
y0	list-data	variable, list
y1	reflist	variable, reflist
y1	list-data	variable, list
y2	reflist	variable, reflist
y2	list-data	variable, list
z	reflist	variable, reflist
z	list-data	variable, list
z0	reflist	variable, reflist
z0	list-data	variable, list
z1	reflist	variable, reflist
z1	list-data	variable, list
z2	reflist	variable, reflist
z2	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
×	linheap	function, Ref × cell → elemdata
×	int-pair	function, int × int → int
×	store	function, elem × data → elemdata
×	pair	function, elem × data → pair
ε	hilbert-choice	function, elem → bool → elem
μ	monotone-set-fixpoint	function, (elem → bool) → elem → bool → elem → bool
ν	monotone-set-fixpoint	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
σx2	stream-of-streams	variable, streamlist
σy	stream-of-streams	variable, streamlist
σy0	stream-of-streams	variable, streamlist
σy1	stream-of-streams	variable, streamlist
σy2	stream-of-streams	variable, streamlist
σz	stream-of-streams	variable, streamlist
σz0	stream-of-streams	variable, streamlist
σz1	stream-of-streams	variable, streamlist
σz2	stream-of-streams	variable, streamlist
σσ	stream-of-streams	variable, streamstream
σσ1	stream-of-streams	variable, streamstream
σσ2	stream-of-streams	variable, streamstream
φ	fixpoint-induction	variable, elem → bool
χ	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, elemdata × heap
∈	linheap	predicate, Ref × heap
∈	infset-basic	predicate, elem × set
∈	assoclist	predicate, elem × assoclist
∈	assoclista	predicate, pair × assoclist
∈	list	predicate, elem × list
∈	array-copy	predicate, elem × array
∈	set-basic	predicate, elem × set
∈	store	predicate, elemdata × store
∈	store	predicate, elem × store
∈	string-new	predicate, char × string
∞	int-inf-basic	constant, intinf
∞	nat-inf-basic	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
⊆	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-new	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
⊑	assoclista	predicate, assoclist × assoclist
⊑	list-last	predicate, list × list
⊑	string-new	predicate, string × string
⊒	natstream	predicate, natlist × natlist
⊒	stream-of-streams	predicate, streamlist × streamlist
⊒	reflist	predicate, reflist × reflist
⊒	assoclista	predicate, assoclist × assoclist
⊒	list-last	predicate, list × list
⊒	string-new	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
⌝	nat-inf-basic	function, nat → natinf
⌝	stream-basic	function, nat → elem → stream
⌝	stream-basic	function, list → stream