[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('a) → nat
#	stream	function, stream('a) → natinf
#	list-data	function, list('a) → nat
#	set-basic	function, set('a) → nat
#	store	function, store('a, 'b) → nat
#	bag-union	function, bag('a) → nat
#	stream-old	function, stream('a) → natinf
#c	matrix	function, matrix('a) → nat
#oc	list-perm	function, 'a × list('a) → nat
#oc	list-as-arrayinstance	function, 'a × array('a) → nat
#r	matrix	function, matrix('a) → nat
#x	cube	function, cube('a) → nat
#y	cube	function, cube('a) → nat
#z	cube	function, cube('a) → nat
'	list	function, 'a → list('a)
'	list-as-arrayinstance	function, 'a → array('a)
*	nat-mult	function, nat × nat → nat
*	matrixops	partial function, array(ring) × array(ring) → ring
*	matrixops	partial function, array(ring) × matrix(ring) → array(ring)
*	matrixops	partial function, matrix(ring) × array(ring) → array(ring)
*	matrixops	partial function, matrix(ring) × matrix(ring) → matrix(ring)
*	ring	function, ring × ring → ring
+	array-listops	function, 'a × array('a) → array('a)
+	matrixops	partial function, array(ring) × array(ring) → array(ring)
+	matrixops	partial function, matrix(ring) × matrix(ring) → matrix(ring)
+	nat-inf	function, natinf × natinf → natinf
+	ring	function, ring × ring → ring
+	list	function, list('a) × 'a → list('a)
+	list	function, list('a) × list('a) → list('a)
+	stream	function, stream('a) × stream('a) → stream('a)
+	stream	function, 'a × stream('a) → stream('a)
+	list-data	function, 'a × list('a) → list('a)
+	list-as-arrayinstance	function, array('a) × 'a → array('a)
+	list-as-arrayinstance	function, array('a) × array('a) → array('a)
+	stream-old	function, stream('a) × stream('a) → stream('a)
+	stream-old	function, 'a × stream('a) → stream('a)
+	nat-basic	function, nat × nat → nat
++	list-dup	function, list('a) × 'a → list('a)
++	set-basic	function, set('a) × 'a → set('a)
++	bag-basic	function, bag('a) × 'a → bag('a)
++	infset-basic	function, iset('a) × 'a → iset('a)
++	list-as-arrayinstance	function, array('a) × 'a → array('a)
+1	nat-basic	function, nat → nat
+2	list	function, 'a × 'a → list('a)
+2	list-as-arrayinstance	function, 'a × 'a → array('a)
-	nat	partial function, nat × nat → nat
--	store	function, store('a, 'b) × 'a → store('a, 'b)
--	set-union	function, set('a) × 'a → set('a)
--	bag-union	function, bag('a) × 'a → bag('a)
--	infset-union	function, iset('a) × 'a → iset('a)
-1	nat-basic	partial function, nat → nat
-1l	list-del	function, list('a) × 'a → list('a)
-1l	list-as-arrayinstance	function, array('a) × 'a → array('a)
-l	list-del	function, list('a) × 'a → list('a)
-l	list-as-arrayinstance	function, array('a) × 'a → array('a)
-p	list-del	function, list('a) × nat → list('a)
-p	list-as-arrayinstance	function, array('a) × nat → array('a)
.butlast	list-last	partial function, list('a) → list('a)
.butlast	list-as-arrayinstance	partial function, array('a) → array('a)
.butmax	oset	partial function, set(tord) → set(tord)
.butmin	oset	partial function, set(tord) → set(tord)
.butmin	ostore	partial function, store(tord, 'b) → store(tord, 'b)
.f	stream-basic	partial function, stream('a) → nat → 'a
.first	array-listops	partial function, array('a) → 'a
.foldLeft	list	function, list('a) × 'b × 'b × 'a → 'b → 'b
.foldLeft	list-as-arrayinstance	function, array('a) × 'b × 'b × 'a → 'b → 'b
.head	list-data	partial function, list('a) → 'a
.keys	ostore	function, store(tord, 'b) → set(tord)
.l	stream-basic	partial function, stream('a) → list('a)
.last	list-last	partial function, list('a) → 'a
.last	list-as-arrayinstance	partial function, array('a) → 'a
.max	oset	partial function, set(tord) → tord
.min	oset	partial function, set(tord) → tord
.min	ostore	partial function, store(tord, 'b) → tord
.n	nat-inf	partial function, natinf → nat
.nxt	lincell	function, cell → Ref
.rest	array-listops	partial function, array('a) → array('a)
.tail	list-data	partial function, list('a) → list('a)
.toArc	rowcol-upd	function, matrix('a) → array('a)
.toArr	rowcol-upd	function, matrix('a) → array('a)
<	array-listops	predicate, array('a) × array('a)
<	oset	predicate, set(tord) × tord
<	oset	predicate, tord × set(tord)
<	nat-inf	predicate, natinf × natinf
<	weakord	predicate, weakord × weakord
<	list-data	predicate, list('a) × list('a)
<	nat-basic	predicate, nat × nat
<	tord	predicate, tord × tord
>	nat	predicate, nat × nat
I	ring	constant, ring
IS	monotone-set-fixpoint	function, ('a → bool) → bool → 'a → bool
O	ring	constant, ring
O-	matrixops	function, array(ring) → array(ring)
O-	matrixops	function, matrix(ring) → matrix(ring)
O-	ring	function, ring → ring
Ref	Ref	sort,
UN	monotone-set-fixpoint	function, ('a → bool) → bool → 'a → bool
[]	array-listops	constant, array('a)
[]	stream	constant, stream('a)
[]	list-data	constant, list('a)
[]	stream-old	constant, stream('a)
\	ostore+set	function, store('a, 'b) × set('a) → store('a, 'b)
\	set-union	function, set('a) × set('a) → set('a)
\	list-as-arrayinstance	function, array('a) × array('a) → array('a)
\	bag-union	function, bag('a) × bag('a) → bag('a)
\	infset-union	function, iset('a) × iset('a) → iset('a)
\	list-set	function, list('a) × list('a) → list('a)
]	list-getput	partial function, list('a) × nat × 'a → list('a)
]	list-getput	partial function, list('a) × nat → 'a
]	array	partial function, array('a) × nat × 'a → array('a)
]	array	partial function, array('a) × nat → 'a
]	assoclist	partial function, list(('a, 'b)) × 'b → 'a
]	assoclist	partial function, list(('a, 'b)) × 'a → 'b
]	assoclist	function, list(('a, 'b)) × 'a × 'b → list(('a, 'b))
]	stream	partial function, stream('a) × nat × 'a → stream('a)
]	stream	partial function, stream('a) × nat → 'a
]	matrix	partial function, matrix('a) × nat × nat × 'a → matrix('a)
]	matrix	partial function, matrix('a) × nat × nat → 'a
]	cube	partial function, cube('a) × nat × nat × nat × 'a → cube('a)
]	cube	partial function, cube('a) × nat × nat × nat → 'a
]	store	partial function, store('a, 'b) × 'a → 'b
]	store	function, store('a, 'b) × 'a × 'b → store('a, 'b)
]	stream-old	partial function, stream('a) × nat × 'a → stream('a)
]	stream-old	partial function, stream('a) × nat → 'a
]c	rowcol-upd	partial function, matrix('a) × nat × array('a) → matrix('a)
]c	matrix+array	partial function, matrix('a) × nat → array('a)
]r	rowcol-upd	partial function, matrix('a) × nat × array('a) → matrix('a)
]r	matrix+array	partial function, matrix('a) × nat → array('a)
]xy	cube+array	partial function, cube('a) × nat × nat → array('a)
]xz	cube+array	partial function, cube('a) × nat × nat → array('a)
]yz	cube+array	partial function, cube('a) × nat × nat → array('a)
^	approx-fixpoint	function, ('a → bool) → 'a → bool × nat → ('a → bool) → 'a → bool
^*	rtc	function, 'a × 'a → bool → 'a × 'a → bool
a	list-getput	variable, 'a
a	array-listops	variable, 'a
a	putoutside-id	variable, 'a
a	array	variable, 'a
a	list-del	variable, 'a
a	olist	variable, tord
a	oset	variable, tord
a	wellfounded	variable, 'a
a	streamseq-mon-lim-old	variable, 'a
a	list-perm	variable, 'a
a	ostore+set	variable, 'a
a	matrixops	variable, ring
a	filter-count	variable, 'a
a	array-as-listinstance	variable, 'a
a	rtc	variable, 'a
a	list-dup	variable, 'a
a	ring	variable, ring
a	ostore	variable, tord
a	array-copy	variable, 'a
a	list	variable, 'a
a	assoclist	variable, 'a
a	infinite-append	variable, 'a
a	olist-min-max	variable, tord
a	tord-min-max	variable, tord
a	stream	variable, 'a
a	weakord	variable, weakord
a	matrix	variable, 'a
a	mon-lim-filter-count-old	variable, 'a
a	list-data	variable, 'a
a	oarray-sort	variable, 'a
a	inf-app-list	variable, 'a
a	list-last	variable, 'a
a	set-basic	variable, 'a
a	rowcol-upd	variable, array('a)
a	bag-basic	variable, 'a
a	mon-lim-filter-count	variable, 'a
a	cube	variable, 'a
a	infset-basic	variable, 'a
a	store	variable, 'a
a	set-union	variable, 'a
a	olist-sort	variable, tord
a	list-as-arrayinstance	variable, 'a
a	bag-union	variable, 'a
a	stream-old	variable, 'a
a	infset-union	variable, 'a
a	infinite-append-old	variable, 'a
a	list-set	variable, 'a
a	streamseq-mon-lim	variable, 'a
a	inf-app-list-old	variable, 'a
a	tord	variable, tord
a	wolist	variable, weakord
a	woarray	variable, 'a
af	wellfounded	variable, 'a → 'a
all<	olist-min-max	predicate, list(tord) × nat × nat × tord
all<	olist-min-max	predicate, list(tord) × tord
all<	oarray-sort	predicate, array(tord) × nat × nat × tord
all<	oarray-sort	predicate, array(tord) × tord
all>	olist-min-max	predicate, list(tord) × nat × nat × tord
all>	olist-min-max	predicate, list(tord) × tord
all>	oarray-sort	predicate, array(tord) × nat × nat × tord
all>	oarray-sort	predicate, array(tord) × tord
all≤	olist-min-max	predicate, list(tord) × nat × nat × tord
all≤	olist-min-max	predicate, list(tord) × tord
all≤	oarray-sort	predicate, array(tord) × nat × nat × tord
all≤	oarray-sort	predicate, array(tord) × tord
all≥	olist-min-max	predicate, list(tord) × nat × nat × tord
all≥	olist-min-max	predicate, list(tord) × tord
all≥	oarray-sort	predicate, array(tord) × nat × nat × tord
all≥	oarray-sort	predicate, array(tord) × tord
ar	array-listops	variable, array('a)
ar	array	variable, array('a)
ar	array-copy	variable, array('a)
ar	oarray-sort	variable, array('a)
ar	list-as-arrayinstance	variable, array('a)
ar	get-outside	variable, array('a)
ar	woarray	variable, array('a)
array	array	sort,
ax	assoclist	variable, list(('a, 'b))
b	list-getput	variable, 'a
b	array	variable, 'a
b	list-del	variable, 'a
b	olist	variable, tord
b	oset	variable, tord
b	wellfounded	variable, 'b
b	streamseq-mon-lim-old	variable, 'a
b	list-perm	variable, 'a
b	filter-count	variable, 'b
b	array-as-listinstance	variable, 'a
b	rtc	variable, 'a
b	list-dup	variable, 'a
b	ring	variable, ring
b	list	variable, 'b
b	assoclist	variable, 'a
b	olist-min-max	variable, tord
b	tord-min-max	variable, tord
b	weakord	variable, weakord
b	matrix	variable, 'a
b	mon-lim-filter-count-old	variable, 'a
b	inf-app-list	variable, 'a
b	list-last	variable, 'a
b	bag-basic	variable, 'a
b	mon-lim-filter-count	variable, 'a
b	cube	variable, 'a
b	infset-basic	variable, 'a
b	store	variable, 'a
b	set-union	variable, 'b
b	olist-sort	variable, tord
b	bag-union	variable, 'a
b	infset-union	variable, 'a
b	list-set	variable, 'a
b	streamseq-mon-lim	variable, 'a
b	inf-app-list-old	variable, 'a
b	tord	variable, tord
b	wolist	variable, weakord
bag	bag-basic	variable, bag('a)
bag	bag-basic	sort,
bag	bag-union	variable, bag('a)
bc	wellfounded	variable, ('b, 'c)
butlastn	list-last	partial function, nat × list('a) → list('a)
butlastn	list-as-arrayinstance	partial function, nat × array('a) → array('a)
c	list-getput	variable, 'a
c	array	variable, 'a
c	olist	variable, tord
c	wellfounded	variable, 'c
c	list-perm	variable, 'a
c	matrixops	variable, nat
c	array-as-listinstance	variable, 'a
c	rtc	variable, 'a
c	list-dup	variable, 'a
c	ring	variable, ring
c	weakord	variable, weakord
c	matrix	variable, nat
c	list-last	variable, 'a
c	rowcol-upd	variable, nat
c	store	variable, 'a
c	olist-sort	variable, tord
c	infset-union	variable, 'a
c	matrix+array	variable, nat
c	list-set	variable, 'a
c	tord	variable, tord
c	wolist	variable, weakord
ce	path-reachable	variable, cell
ce	lincell	variable, cell
cell	lincell	sort,
chain	approx-fixpoint	predicate, nat → 'a → bool
chn	wellfounded	variable, nat → 'a
chn	approx-fixpoint	variable, nat → 'a → bool
chngen	wellfounded	variable, nat → nat → 'a
cmp	array-copy	partial predicate, array('a) × 'a × nat × nat
cmp	array-copy	partial predicate, array('a) × nat × array('a) × nat × nat
cmp	array-copy	predicate, array('a) × 'a
cnt	mon-lim-filter-count-old	function, 'a × stream('a) → natinf
cnt	mon-lim-filter-count	function, 'a × stream('a) → natinf
compl	monotone-set-fixpoint	function, ('a → bool) → 'a → bool → ('a → bool) → 'a → bool
cont	approx-fixpoint	predicate, ('a → bool) → 'a → bool
copy	array-copy	partial function, array('a) × nat × array('a) × nat × nat → array('a)
count	filter-count	partial function, list('a) × nat × nat × 'a → bool → nat
count	filter-count	function, list('a) × 'a → bool → nat
count	oarray-sort	partial function, array('a) × nat × nat × 'a → bool → nat
count	oarray-sort	function, array('a) × 'a → bool → nat
count	bag-basic	function, 'a × bag('a) → nat
cu	cube	variable, cube('a)
cu	cube+array	variable, cube('a)
cube	cube	sort,
d	ostore+set	variable, 'b
d	ostore	variable, 'b
d	assoclist	variable, 'b
d	store	variable, 'b
disj	list-dup	predicate, list('a) × list('a)
disj	list-as-arrayinstance	predicate, array('a) × array('a)
disjoint	set-union	predicate, set('a) × set('a)
dom	ostore+set	function, store('a, 'b) → set('a)
dups	list-dup	predicate, list('a)
dups	list-as-arrayinstance	predicate, array('a)
f	matrixops	variable, nat → ring
f	stream-basic	variable, nat → 'a
f	list	variable, 'a → 'b
f	infinite-append	variable, 'a → 'a
f	approx-fixpoint	variable, ('a → bool) → 'a → bool
f	infset-basic	variable, 'a → bool
f	set-union	variable, 'a → 'b
f	monotone-set-fixpoint	variable, ('a → bool) → 'a → bool
fill	array-copy	partial function, array('a) × 'a × nat × nat → array('a)
fill	array-copy	function, array('a) × 'a → array('a)
fillfirst	list-last	function, nat × 'a × list('a) → list('a)
fillfirst	list-as-arrayinstance	function, nat × 'a × array('a) → array('a)
filter	filter-count	function, list('a) × 'a → bool → list('a)
filter	mon-lim-filter-count-old	function, 'a → bool × stream('a) → stream('a)
filter	oarray-sort	function, array('a) × 'a → bool → array('a)
filter	mon-lim-filter-count	function, 'a → bool × stream('a) → stream('a)
filter	set-union	function, set('a) × 'a → bool → set('a)
filter	list-as-arrayinstance	function, array('a) × array('a) → array('a)
filter	list-set	function, list('a) × list('a) → list('a)
finp	stream-basic	predicate, stream('a)
firstn	list-del	partial function, nat × list('a) → list('a)
firstn	list-as-arrayinstance	partial function, nat × array('a) → array('a)
from	stream	partial function, list('a) × nat → list('a)
from	stream	partial function, stream('a) × nat → stream('a)
from	stream	function, nat → 'a × nat → nat → 'a
from	stream-old	partial function, list('a) × nat → list('a)
from	stream-old	partial function, stream('a) × nat → stream('a)
from	stream-old	function, nat → 'a × nat → nat → 'a
frome	list-del	function, list('a) × 'a → list('a)
frome	list-as-arrayinstance	function, array('a) × 'a → array('a)
g	matrixops	variable, nat × nat → ring
h	path-reachable	variable, store(Ref, cell)
hd	stream	partial function, stream('a) → 'a
hd	stream-old	partial function, stream('a) → 'a
head	list-data	variable, 'a
i	rowcol-upd	variable, 'a
idrange	array-copy	partial predicate, array('a) × nat × nat
id○	array-copy	predicate, array('a) × array('a) × nat × nat
id○	array-copy	predicate, array('a) × array('a) × nat
ii	infinite-append	variable, nat → nat
ii	inf-app-list	variable, nat → nat
ii	infinite-append-old	variable, nat → nat
ii	streamseq-mon-lim	variable, nat → nat
ii	inf-app-list-old	variable, nat → nat
iigen	infinite-append	variable, nat → nat → nat
iigen	infinite-append-old	variable, nat → nat → nat
ins≤	olist	function, tord × list(tord) → list(tord)
ins≤	oarray-sort	function, tord × array(tord) → array(tord)
ins≤	wolist	function, weakord × list(weakord) → list(weakord)
ins≤	woarray	function, weakord × array(weakord) → array(weakord)
inv	stut-mon-old	partial function, stream(nat) → stream(nat)
inv	stut-mon	partial function, stream(nat) → stream(nat)
iset	approx-fixpoint	variable, 'a → bool
iset	infset-basic	sort,
iset	monotone-set-fixpoint	variable, 'a → bool
iset0	monotone-set-fixpoint	variable, 'a → bool
iset1	monotone-set-fixpoint	variable, 'a → bool
isetset	monotone-set-fixpoint	variable, ('a → bool) → bool
j	rowcol-upd	variable, 'a
jj	infinite-append	variable, nat → nat
jj	infinite-append-old	variable, nat → nat
l	stream-basic	variable, list('a)
lastn	list-del	partial function, nat × list('a) → list('a)
lastn	list-as-arrayinstance	partial function, nat × array('a) → array('a)
lastoc	mon-lim-filter-count-old	function, 'a × stream('a) → natinf
lastoc	mon-lim-filter-count	function, 'a × stream('a) → natinf
leninv	stut-mon-old	function, stream(nat) → natinf
leninv	stut-mon	function, stream(nat) → natinf
lf	infinite-append	variable, nat → list('a)
lf	inf-app-list	variable, nat → list('a)
lf	infinite-append-old	variable, nat → list('a)
lf	streamseq-mon-lim	variable, nat → list('a)
lf	inf-app-list-old	variable, nat → list('a)
lfgen	infinite-append	variable, nat → nat → list('a)
lfgen	infinite-append-old	variable, nat → nat → list('a)
lim	streamseq-mon-lim-old	partial function, stream(stream('a)) → stream('a)
lim	mon-lim-filter-count-old	partial function, nat → stream('a) → stream('a)
lim	mon-lim-filter-count	partial function, nat → stream('a) → stream('a)
lim	streamseq-mon-lim	partial function, stream(stream('a)) → stream('a)
list	list-data	sort,
m	list-getput	variable, nat
m	putoutside-id	variable, nat
m	array	variable, nat
m	list-del	variable, nat
m	olist	variable, nat
m	streamseq-mon-lim-old	variable, nat
m	nat-mult	variable, nat
m	list-perm	variable, nat
m	matrixops	variable, nat
m	filter-count	variable, nat
m	array-as-listinstance	variable, nat
m	nat-inf	variable, nat
m	stream-basic	variable, nat
m	array-copy	variable, nat
m	infinite-append	variable, nat
m	olist-min-max	variable, nat
m	stream	variable, nat
m	mon-lim-filter-count-old	variable, nat
m	approx-fixpoint	variable, nat
m	inf-app-list	variable, nat
m	rowcol-upd	variable, nat
m	mon-lim-filter-count	variable, nat
m	stream-old	variable, nat
m	path-reachable	variable, nat
m	infinite-append-old	variable, nat
m	natset	variable, nat
m	list-set	variable, nat
m	streamseq-mon-lim	variable, nat
m	stut-mon	variable, nat
m	inf-app-list-old	variable, nat
m	wolist	variable, nat
map	list	function, list('a) × 'a → 'b → list('b)
map	set-union	function, set('a) × 'a → 'b → set('b)
map	list-as-arrayinstance	function, array('a) × 'a → 'b → array('b)
matrix	matrix	sort,
max	olist-min-max	partial function, list(tord) → tord
max	tord-min-max	function, tord × tord → tord
max	oarray-sort	partial function, array(tord) → tord
max∞	stut-mon-old	function, nat → bool → natinf
max∞	stut-mon	function, nat → bool → natinf
merge	olist	function, list(tord) × list(tord) → list(tord)
merge	oarray-sort	function, array(tord) × array(tord) → array(tord)
merge	wolist	function, list(weakord) × list(weakord) → list(weakord)
merge	woarray	function, array(weakord) × array(weakord) → array(weakord)
min	stut-mon-old	partial function, stream(nat) × nat → nat
min	nat-inf	function, natinf × natinf → natinf
min	olist-min-max	partial function, list(tord) → tord
min	tord-min-max	function, tord × tord → tord
min	oarray-sort	partial function, array(tord) → tord
min	stut-mon	partial function, stream(nat) × nat → nat
mkarray	array	function, nat → array('a)
mkcube	cube	function, nat × nat × nat × 'a → cube('a)
mklist	list-last	function, 'a × nat → list('a)
mklist	list-as-arrayinstance	function, 'a × nat → array('a)
mkmatrix	matrix	function, nat × nat × 'a → matrix('a)
mon	streamseq-mon-lim-old	predicate, stream(stream('a))
mon	mon-lim-filter-count-old	predicate, nat → stream('a)
mon	mon-lim-filter-count	predicate, nat → stream('a)
mon	streamseq-mon-lim	predicate, stream(stream('a))
mon<	stut-mon-old	predicate, stream(nat)
mon<	stut-mon	predicate, stream(nat)
monotone	monotone-set-fixpoint	predicate, ('a → bool) → 'a → bool
mon≤	stut-mon-old	predicate, stream(nat)
mon≤	stut-mon	predicate, stream(nat)
mx	matrixops	variable, matrix(ring)
mx	matrix	variable, matrix('a)
mx	rowcol-upd	variable, matrix('a)
mx	matrix+array	variable, matrix('a)
n	list-getput	variable, nat
n	array-listops	variable, nat
n	putoutside-id	variable, nat
n	array	variable, nat
n	list-del	variable, nat
n	olist	variable, nat
n	streamseq-mon-lim-old	variable, nat
n	stut-mon-old	variable, nat
n	nat-mult	variable, nat
n	list-perm	variable, nat
n	matrixops	variable, nat
n	filter-count	variable, nat
n	array-as-listinstance	variable, nat
n	nat-inf	variable, nat
n	rtc	variable, nat
n	array-copy	variable, nat
n	infinite-append	variable, nat
n	olist-min-max	variable, nat
n	stream	variable, nat
n	mon-lim-filter-count-old	variable, nat
n	list-data	variable, nat
n	oarray-sort	variable, nat
n	approx-fixpoint	variable, nat
n	inf-app-list	variable, nat
n	list-last	variable, nat
n	rowcol-upd	variable, nat
n	mon-lim-filter-count	variable, nat
n	list-as-arrayinstance	variable, nat
n	stream-old	variable, nat
n	path-reachable	variable, nat
n	get-outside	variable, nat
n	infinite-append-old	variable, nat
n	natset	variable, nat
n	list-set	variable, nat
n	streamseq-mon-lim	variable, nat
n	stut-mon	variable, nat
n	inf-app-list-old	variable, nat
n	wolist	variable, nat
n	woarray	variable, nat
nat	nat-basic	sort,
natinf	nat-inf	sort,
nexta	infinite-append	variable, nat × 'a → 'a
nextj	infinite-append	variable, nat × 'a → nat
nextj	infinite-append-old	variable, nat × 'a → nat
nextl	infinite-append	variable, nat × 'a → list('a)
nextl	infinite-append-old	variable, nat × 'a → list('a)
nextli	inf-app-list	variable, list('a) → list('a)
nextli	inf-app-list-old	variable, list('a) → list('a)
nextnli	inf-app-list	variable, list('a) × nat → list('a)
nextnli	inf-app-list-old	variable, list('a) × nat → list('a)
nf	streamseq-mon-lim-old	variable, nat → 'a
nf	stut-mon-old	variable, nat → nat
nf	stream-basic	variable, nat → 'a
nf	infinite-append	variable, nat → 'a
nf	stream	variable, nat → 'a
nf	mon-lim-filter-count-old	variable, nat → 'a
nf	mon-lim-filter-count	variable, nat → 'a
nf	stream-old	variable, nat → 'a
nf	infinite-append-old	variable, nat → 'a
nf	streamseq-mon-lim	variable, nat → 'a
nf	stut-mon	variable, nat → nat
nfgen	infinite-append	variable, nat → nat → 'a
nfgen	infinite-append-old	variable, nat → nat → 'a
nl	stut-mon-old	variable, list(nat)
nl	stut-mon	variable, list(nat)
nnf	streamseq-mon-lim-old	variable, nat → nat
nnf	stut-mon-old	variable, nat → nat
nnf	mon-lim-filter-count-old	variable, nat → nat
nnf	mon-lim-filter-count	variable, nat → nat
nnf	streamseq-mon-lim	variable, nat → nat
nnf	stut-mon	variable, nat → nat
np	streamseq-mon-lim-old	variable, nat → bool
np	stut-mon-old	variable, nat → bool
np	mon-lim-filter-count-old	variable, nat → bool
np	mon-lim-filter-count	variable, nat → bool
np	streamseq-mon-lim	variable, nat → bool
np	stut-mon	variable, nat → bool
ns	matrixops	variable, set(nat)
ns	natset	variable, set(nat)
null	Ref	constant, Ref
nx	cube	variable, nat
nx	cube+array	variable, nat
ny	cube	variable, nat
ny	cube+array	variable, nat
nz	cube	variable, nat
nz	cube+array	variable, nat
nσ	stut-mon-old	variable, stream(nat)
nσ	stut-mon	variable, stream(nat)
nσf	stut-mon-old	variable, nat → stream(nat)
nσf	stut-mon	variable, nat → stream(nat)
n∞	streamseq-mon-lim-old	variable, natinf
n∞	stut-mon-old	variable, natinf
n∞	nat-inf	variable, natinf
n∞	stream	variable, natinf
n∞	mon-lim-filter-count-old	variable, natinf
n∞	mon-lim-filter-count	variable, natinf
n∞	stream-old	variable, natinf
n∞	streamseq-mon-lim	variable, natinf
n∞	stut-mon	variable, natinf
ordered<	olist	predicate, list(tord)
ordered<	oarray-sort	predicate, array(tord)
ordered<	wolist	predicate, list(weakord)
ordered<	woarray	predicate, array(weakord)
ordered≤	olist	predicate, list(tord)
ordered≤	oarray-sort	predicate, array(tord)
ordered≤	wolist	predicate, list(weakord)
ordered≤	woarray	predicate, array(weakord)
p	wellfounded	variable, 'a → bool
p	streamseq-mon-lim-old	variable, 'a → bool
p	stut-mon-old	variable, 'a → bool
p	filter-count	variable, 'a → bool
p	assoclist	variable, ('a, 'b)
p	mon-lim-filter-count-old	variable, 'a → bool
p	mon-lim-filter-count	variable, 'a → bool
p	set-union	variable, 'a → bool
p	streamseq-mon-lim	variable, 'a → bool
p	stut-mon	variable, 'a → bool
path	path-reachable	predicate, list(Ref) × store(Ref, cell)
pelem	rtc	variable, 'a × 'a → bool
perm	list-perm	predicate, list('a) × list('a)
perm	list-as-arrayinstance	predicate, array('a) × array('a)
pos	list-del	function, 'a × list('a) → nat
pos	list-as-arrayinstance	function, 'a × array('a) → nat
q	wellfounded	variable, 'b × 'c → bool
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 × store(Ref, cell)
reachable*	path-reachable	predicate, store(Ref, cell) × Ref × Ref
reachable-1	path-reachable	predicate, store(Ref, cell) × Ref × Ref
reachable-n	path-reachable	predicate, store(Ref, cell) × nat × Ref × Ref
rem	mon-lim-filter-count-old	function, stream('a) × nat → bool → stream('a)
rem	mon-lim-filter-count	function, stream('a) × nat → bool → stream('a)
restn	list-del	partial function, nat × list('a) → list('a)
restn	list-as-arrayinstance	partial function, nat × array('a) → array('a)
rev	list-last	function, list('a) → list('a)
rev	list-as-arrayinstance	function, array('a) → array('a)
ring	ring	sort,
rmdup	list-dup	function, list('a) → list('a)
rmdup	list-as-arrayinstance	function, array('a) → array('a)
rtc	rtc	function, nat × 'a × 'a → bool → 'a × 'a → bool
s	oset	variable, set(tord)
s	ostore+set	variable, set('a)
s	ostore	variable, set(tord)
s	set-basic	variable, set('a)
s	infset-basic	variable, iset('a)
s	set-union	variable, set('a)
s	infset-union	variable, iset('a)
set	set-basic	sort,
sort	oarray-sort	function, array(tord) → array(tord)
sort	olist-sort	function, list(tord) → list(tord)
st	ostore+set	variable, store('a, 'b)
st	ostore	variable, store(tord, 'b)
st	store	variable, store('a, 'b)
store	store	sort,
stream	stream-basic	sort,
stutf	stut-mon-old	predicate, stream(nat)
stutf	stut-mon	predicate, stream(nat)
subarray	array-copy	partial function, array('a) × nat × nat → array('a)
sublist	list-del	partial function, nat × nat × list('a) → list('a)
sublist	list-as-arrayinstance	partial function, nat × nat × array('a) → array('a)
tail	list-data	variable, list('a)
tl	stream	partial function, stream('a) → stream('a)
tl	stream-old	partial function, stream('a) → stream('a)
to	stream	partial function, list('a) × nat → list('a)
to	stream	partial function, stream('a) × nat → list('a)
to	stream	function, nat → 'a × nat → list('a)
to	stream-old	partial function, list('a) × nat → list('a)
to	stream-old	partial function, stream('a) × nat → stream('a)
to	stream-old	function, nat → 'a × nat → list('a)
to	natset	function, nat × nat → set(nat)
toArc	rowcol-upd	function, matrix('a) × nat → array('a)
toArr	rowcol-upd	function, matrix('a) × nat → array('a)
tord	tord	sort,
to∞	stream	partial function, stream('a) × natinf → stream('a)
to∞	stream-old	partial function, stream('a) × natinf → stream('a)
trans	wellfounded	predicate, 'a × 'a → bool
twf	wellfounded	predicate, 'a × 'a → bool
twfinv	wellfounded	predicate, 'a × 'a → bool
unique_al	assoclist	predicate, list(('a, 'b))
vec	matrixops	variable, array(ring)
weakord	weakord	sort,
wf	wellfounded	predicate, 'a × 'a → bool
wf1≪	wellfounded	variable, 'b × 'b → bool
wf2≪	wellfounded	variable, 'c × 'c → bool
wfinv	wellfounded	predicate, 'a × 'a → bool
wf≪	wellfounded	variable, 'a × 'a → bool
wf≫	wellfounded	variable, 'a × 'a → bool
x	list-getput	variable, list('a)
x	putoutside-id	variable, list('a)
x	list-del	variable, list('a)
x	olist	variable, list(tord)
x	streamseq-mon-lim-old	variable, list('a)
x	list-perm	variable, list('a)
x	filter-count	variable, list('a)
x	array-as-listinstance	variable, list('a)
x	stream-basic	variable, list('a)
x	list-dup	variable, list('a)
x	list	variable, list('a)
x	olist-min-max	variable, list(tord)
x	stream	variable, list('a)
x	mon-lim-filter-count-old	variable, list('a)
x	list-data	variable, list('a)
x	approx-fixpoint	variable, 'a
x	inf-app-list	variable, list('a)
x	list-last	variable, list('a)
x	mon-lim-filter-count	variable, list('a)
x	olist-sort	variable, list(tord)
x	monotone-set-fixpoint	variable, 'a
x	stream-old	variable, list('a)
x	path-reachable	variable, list(Ref)
x	list-set	variable, list('a)
x	streamseq-mon-lim	variable, list('a)
x	inf-app-list-old	variable, list('a)
x	wolist	variable, list(weakord)
x0	monotone-set-fixpoint	variable, 'a
x1	monotone-set-fixpoint	variable, 'a
y	list-getput	variable, list('a)
y	list-del	variable, list('a)
y	olist	variable, list(tord)
y	list-perm	variable, list('a)
y	filter-count	variable, list('a)
y	array-as-listinstance	variable, list('a)
y	list-dup	variable, list('a)
y	list	variable, list('a)
y	olist-min-max	variable, list('a)
y	stream	variable, list('a)
y	list-data	variable, list('a)
y	inf-app-list	variable, list('a)
y	list-last	variable, list('a)
y	olist-sort	variable, list(tord)
y	stream-old	variable, list('a)
y	path-reachable	variable, list(Ref)
y	list-set	variable, list('a)
y	inf-app-list-old	variable, list('a)
y	wolist	variable, list(weakord)
z	list-getput	variable, list('a)
z	list-del	variable, list('a)
z	olist	variable, list(tord)
z	list-perm	variable, list('a)
z	filter-count	variable, list('b)
z	array-as-listinstance	variable, list('a)
z	list-dup	variable, list('a)
z	list	variable, list('a)
z	stream	variable, list('a)
z	list-data	variable, list('a)
z	list-last	variable, list('a)
z	olist-sort	variable, list(tord)
z	stream-old	variable, list('a)
z	list-set	variable, list('a)
z	wolist	variable, list(weakord)
zip	filter-count	function, list('a) × list('b) → list(('a, 'b))
zip	oarray-sort	function, array('a) × array('b) → array(('a, 'b))
\|	ostore+set	function, store('a, 'b) × set('a) → store('a, 'b)
}	infset-basic	function, 'a → bool → iset('a)
}	set-union	function, 'a → set('a)
}	bag-union	function, 'a → bag('a)
}	infset-union	function, 'a → iset('a)
Σ	matrixops	function, set(nat) × nat → ring → ring
μ	monotone-set-fixpoint	partial function, ('a → bool) → 'a → bool → 'a → bool
ν	monotone-set-fixpoint	partial function, ('a → bool) → 'a → bool → 'a → bool
σ	streamseq-mon-lim-old	variable, stream('a)
σ	stream-basic	variable, stream('a)
σ	infinite-append	variable, stream('a)
σ	stream	variable, stream('a)
σ	mon-lim-filter-count-old	variable, stream('a)
σ	inf-app-list	variable, stream('a)
σ	mon-lim-filter-count	variable, stream('a)
σ	stream-old	variable, stream('a)
σ	infinite-append-old	variable, stream('a)
σ	streamseq-mon-lim	variable, stream('a)
σ	inf-app-list-old	variable, stream('a)
σf	streamseq-mon-lim-old	variable, nat → stream('a)
σf	stut-mon-old	variable, nat → stream('a)
σf	mon-lim-filter-count-old	variable, nat → stream('a)
σf	mon-lim-filter-count	variable, nat → stream('a)
σf	streamseq-mon-lim	variable, nat → stream('a)
σf	stut-mon	variable, nat → stream('a)
σσ	streamseq-mon-lim-old	variable, stream(stream('a))
σσ	streamseq-mon-lim	variable, stream(stream('a))
χ	infset-basic	function, iset('a) → 'a → bool
∅	set-basic	constant, set('a)
∅	bag-basic	constant, bag('a)
∅	infset-basic	constant, iset('a)
∅	store	constant, store('a, 'b)
∈	ostore+set	predicate, 'b × store('a, 'b)
∈	list	predicate, 'a × list('a)
∈	assoclist	predicate, 'a × list(('a, 'b))
∈	set-basic	predicate, 'a × set('a)
∈	infset-basic	predicate, 'a × iset('a)
∈	store	predicate, 'a × store('a, 'b)
∈	list-as-arrayinstance	predicate, 'a × array('a)
∈	bag-union	predicate, 'a × bag('a)
∞	nat-inf	constant, natinf
∩	set-union	function, set('a) × set('a) → set('a)
∩	infset-union	function, iset('a) × iset('a) → iset('a)
∪	set-union	function, set('a) × set('a) → set('a)
∪	list-as-arrayinstance	function, array('a) × array('a) → array('a)
∪	bag-union	function, bag('a) × bag('a) → bag('a)
∪	infset-union	function, iset('a) × iset('a) → iset('a)
∪	list-set	function, list('a) × list('a) → list('a)
≤	nat	predicate, nat × nat
≥	nat	predicate, nat × nat
⊆	set-basic	predicate, set('a) × set('a)
⊆	infset-basic	predicate, iset('a) × iset('a)
⊆	store	predicate, store('a, 'b) × store('a, 'b)
⊆	monotone-set-fixpoint	predicate, 'a → bool × 'a → bool
⊆	list-as-arrayinstance	predicate, array('a) × array('a)
⊆	bag-union	predicate, bag('a) × bag('a)
⊆	list-set	predicate, list('a) × list('a)
⊆m	list-perm	predicate, list('a) × list('a)
⊆m	list-as-arrayinstance	predicate, array('a) × array('a)
⊑	stream	predicate, stream('a) × stream('a)
⊑	list-last	predicate, list('a) × list('a)
⊑	list-as-arrayinstance	predicate, array('a) × array('a)
⊑	stream-old	predicate, stream('a) × stream('a)
⊒	list-last	predicate, list('a) × list('a)
⊒	list-as-arrayinstance	predicate, array('a) × array('a)
⊕	ostore+set	function, store('a, 'b) × store('a, 'b) → store('a, 'b)
⌝	nat-inf	function, nat → natinf
⌝	stream-basic	function, nat → 'a → stream('a)
⌝	stream-basic	function, list('a) → stream('a)