[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
#	map	function, Map('a, 'b) → Nat
#	array	function, Array('a) → Nat
#	stream	function, Stream('a) → Natinf
#	list-data	function, List('a) → Nat
#	set-basic	function, Set('a) → 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, List('a) × Nat → 'a → Nat → '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
--	map	function, Map('a, 'b) × 'a → Map('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	omap	partial function, Map(Tord, 'b) → Map(Tord, 'b)
.count	filter-count	partial function, List('a) × Nat × Nat × 'a → Bool → Nat
.count	filter-count	function, List('a) × 'a → Bool → Nat
.count	bag-basic	function, Bag('a) × 'a → Nat
.count	list-as-arrayinstance	partial function, Array('a) × Nat × Nat × 'a → Bool → Nat
.count	list-as-arrayinstance	function, Array('a) × 'a → Bool → Nat
.distinct	list-dup	function, List('a) → List('a)
.distinct	list-as-arrayinstance	function, Array('a) → Array('a)
.drop	list-del	partial function, List('a) × Nat → List('a)
.drop	stream	partial function, Stream('a) × Nat → Stream('a)
.drop	stream	function, Nat → 'a × Nat → Nat → 'a
.drop	list-as-arrayinstance	partial function, Array('a) × Nat → Array('a)
.drop	stream-old	partial function, Stream('a) × Nat → Stream('a)
.drop	stream-old	function, Nat → 'a × Nat → Nat → 'a
.dropRight	list-last	partial function, List('a) × Nat → List('a)
.dropRight	list-as-arrayinstance	partial function, Array('a) × Nat → Array('a)
.exists	forall-indexWhere	predicate, List('a) × 'a → Bool
.f	stream-basic	partial function, Stream('a) → Nat → 'a
.filter	filter-count	function, List('a) × 'a → Bool → List('a)
.filter	mon-lim-filter-count-old	function, Stream('a) × 'a → Bool → Stream('a)
.filter	mon-lim-filter-count	function, Stream('a) × 'a → Bool → Stream('a)
.filter	set-union	function, Set('a) × 'a → Bool → Set('a)
.filter	list-as-arrayinstance	function, Array('a) × 'a → Bool → Array('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
.forall	forall-indexWhere	predicate, List('a) × 'a → Bool
.get	option	partial function, Option('a) → 'a
.getL	either	partial function, Either('a, 'b) → 'a
.getOrElse	option	function, Option('a) × 'a → 'a
.getR	either	partial function, Either('a, 'b) → 'b
.head	list-data	partial function, List('a) → 'a
.indexOf	list-del	function, List('a) × 'a → Nat
.indexOf	list-as-arrayinstance	function, Array('a) × 'a → Nat
.indexWhere	forall-indexWhere	function, List('a) × 'a → Bool → Nat
.isRight	either	predicate, Either('a, 'b)
.keys	omap	function, Map(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
.map	option	function, Option('a) × 'a → 'b → Option('b)
.map	map-ops	function, Map('a, 'b) × 'a × 'b → 'c → Map('a, 'c)
.map	map-ops	function, Map('a, 'b) × 'b → 'c → Map('a, 'c)
.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)
.max	oset	partial function, Set(Tord) → Tord
.min	oset	partial function, Set(Tord) → Tord
.min	omap	partial function, Map(Tord, 'b) → Tord
.n	nat-inf	partial function, Natinf → Nat
.nxt	lincell	function, Cell → Ref
.rest	array-listops	partial function, Array('a) → Array('a)
.sublist	list-del	partial function, List('a) × Nat × Nat → List('a)
.sublist	list-as-arrayinstance	partial function, Array('a) × Nat × Nat → Array('a)
.tail	list-data	partial function, List('a) → List('a)
.take	list-del	partial function, List('a) × Nat → List('a)
.take	stream	partial function, Stream('a) × Natinf → Stream('a)
.take	stream	partial function, Stream('a) × Nat → List('a)
.take	stream	function, Nat → 'a × Nat → List('a)
.take	list-as-arrayinstance	partial function, Array('a) × Nat → Array('a)
.take	stream-old	partial function, Stream('a) × Natinf → Stream('a)
.take	stream-old	partial function, Stream('a) × Nat → Stream('a)
.take	stream-old	function, Nat → 'a × Nat → List('a)
.takeRight	list-del	partial function, List('a) × Nat → List('a)
.takeRight	list-as-arrayinstance	partial function, Array('a) × Nat → Array('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)
<	tord	predicate, Tord × Tord
<	nat-basic	predicate, Nat × Nat
>	nat	predicate, Nat × Nat
Array	array	sort,
Bag	bag-basic	sort,
Cell	lincell	sort,
Cube	cube	sort,
Either	either	sort,
I	ring	constant, Ring
IS	monotone-set-fixpoint	function, ('a → Bool) → Bool → 'a → Bool
Iset	infset-basic	sort,
Left	either	function, 'a → Either('a, 'b)
List	list-data	sort,
Map	map	sort,
Matrix	matrix	sort,
Nat	nat-basic	sort,
Natinf	nat-inf	sort,
None	option	constant, Option('a)
O	ring	constant, Ring
O-	matrixops	function, Array(Ring) → Array(Ring)
O-	matrixops	function, Matrix(Ring) → Matrix(Ring)
O-	ring	function, Ring → Ring
Option	option	sort,
Ref	Ref	sort,
Right	either	function, 'b → Either('a, 'b)
Ring	ring	sort,
Set	set-basic	sort,
Some	option	function, 'a → Option('a)
Stream	stream-basic	sort,
Tord	tord	sort,
UN	monotone-set-fixpoint	function, ('a → Bool) → Bool → 'a → Bool
Weakord	weakord	sort,
[]	array-listops	constant, Array('a)
[]	stream	constant, Stream('a)
[]	list-data	constant, List('a)
[]	stream-old	constant, Stream('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)
\	map+set	function, Map('a, 'b) × Set('a) → Map('a, 'b)
\	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
]	map	partial function, Map('a, 'b) × 'a → 'b
]	map	function, Map('a, 'b) × 'a × 'b → Map('a, 'b)
]	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
]	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	map	variable, 'a
a	array-listops	variable, 'a
a	putoutside-id	variable, 'a
a	array	variable, 'a
a	list-del	variable, 'a
a	woarray	variable, 'a
a	olist	variable, Tord
a	oset	variable, Tord
a	wellfounded	variable, 'a
a	map-ops	variable, 'a
a	streamseq-mon-lim-old	variable, 'a
a	wolist	variable, Weakord
a	list-perm	variable, 'a
a	matrixops	variable, Ring
a	filter-count	variable, 'a
a	array-as-listinstance	variable, 'a
a	forall-indexWhere	variable, 'a
a	rtc	variable, 'a
a	list-dup	variable, 'a
a	ring	variable, Ring
a	omap	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	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	map+set	variable, 'a
a	infinite-append-old	variable, 'a
a	tord	variable, Tord
a	list-set	variable, 'a
a	streamseq-mon-lim	variable, 'a
a	either	variable, 'a
a	inf-app-list-old	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	woarray	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)
ax	assoclist	variable, List(('a, 'b))
b	list-getput	variable, 'a
b	map	variable, 'a
b	array	variable, 'a
b	list-del	variable, 'a
b	olist	variable, Tord
b	oset	variable, Tord
b	wellfounded	variable, 'b
b	map-ops	variable, 'b
b	streamseq-mon-lim-old	variable, 'a
b	wolist	variable, Weakord
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	set-union	variable, 'b
b	olist-sort	variable, Tord
b	bag-union	variable, 'a
b	infset-union	variable, 'a
b	tord	variable, Tord
b	list-set	variable, 'a
b	streamseq-mon-lim	variable, 'a
b	either	variable, 'b
b	inf-app-list-old	variable, 'a
bag	bag-basic	variable, Bag('a)
bag	bag-union	variable, Bag('a)
bc	wellfounded	variable, ('b, 'c)
c	list-getput	variable, 'a
c	map	variable, 'a
c	array	variable, 'a
c	olist	variable, Tord
c	wellfounded	variable, 'c
c	map-ops	variable, 'c
c	wolist	variable, Weakord
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	olist-sort	variable, Tord
c	infset-union	variable, 'a
c	matrix+array	variable, Nat
c	tord	variable, Tord
c	list-set	variable, 'a
ce	path-reachable	variable, Cell
ce	lincell	variable, Cell
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)
cu	cube	variable, Cube('a)
cu	cube+array	variable, Cube('a)
d	map	variable, 'b
d	omap	variable, 'b
d	assoclist	variable, 'b
d	map+set	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	map+set	function, Map('a, 'b) → Set('a)
dups	list-dup	predicate, List('a)
dups	list-as-arrayinstance	predicate, Array('a)
either	either	variable, Either('a, 'b)
f	option	variable, 'a → 'b
f	list-del	variable, 'a → 'b
f	map-ops	variable, 'b → 'c
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)
finp	stream-basic	predicate, Stream('a)
frome	list-del	function, List('a) × 'a → List('a)
frome	list-as-arrayinstance	function, Array('a) × 'a → Array('a)
g	map-ops	variable, 'a × 'b → 'c
g	matrixops	variable, Nat × Nat → Ring
getL	either	variable, 'a
getR	either	variable, 'b
h	path-reachable	variable, Map(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≤	woarray	function, Weakord × Array(Weakord) → Array(Weakord)
ins≤	olist	function, Tord × List(Tord) → List(Tord)
ins≤	wolist	function, Weakord × List(Weakord) → List(Weakord)
ins≤	oarray-sort	function, Tord × Array(Tord) → Array(Tord)
intersect	list-as-arrayinstance	function, Array('a) × Array('a) → Array('a)
intersect	list-set	function, List('a) × List('a) → List('a)
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	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)
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)
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	stut-mon-old	variable, Nat
m	nat-mult	variable, Nat
m	wolist	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	list-last	variable, Nat
m	rowcol-upd	variable, Nat
m	mon-lim-filter-count	variable, Nat
m	set-union	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
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	woarray	function, Array(Weakord) × Array(Weakord) → Array(Weakord)
merge	olist	function, List(Tord) × List(Tord) → List(Tord)
merge	wolist	function, List(Weakord) × List(Weakord) → List(Weakord)
merge	oarray-sort	function, Array(Tord) × Array(Tord) → Array(Tord)
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 × 'a → Array('a)
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	woarray	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	wolist	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	set-union	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
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
opt	option	variable, Option('a)
ordered<	woarray	predicate, Array(Weakord)
ordered<	olist	predicate, List(Tord)
ordered<	wolist	predicate, List(Weakord)
ordered<	oarray-sort	predicate, Array(Tord)
ordered≤	woarray	predicate, Array(Weakord)
ordered≤	olist	predicate, List(Tord)
ordered≤	wolist	predicate, List(Weakord)
ordered≤	oarray-sort	predicate, Array(Tord)
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	forall-indexWhere	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) × Map(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)
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 × Map(Ref, Cell)
reachable*	path-reachable	predicate, Map(Ref, Cell) × Ref × Ref
reachable-1	path-reachable	predicate, Map(Ref, Cell) × Ref × Ref
reachable-n	path-reachable	predicate, Map(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)
rev	list-last	function, List('a) → List('a)
rev	list-as-arrayinstance	function, Array('a) → Array('a)
rtc	rtc	function, Nat × 'a × 'a → Bool → 'a × 'a → Bool
s	oset	variable, Set(Tord)
s	omap	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)
s	map+set	variable, Set('a)
sort	oarray-sort	function, Array(Tord) → Array(Tord)
sort	olist-sort	function, List(Tord) → List(Tord)
st	map	variable, Map('a, 'b)
st	omap	variable, Map(Tord, 'b)
st	map+set	variable, Map('a, 'b)
stutf	stut-mon-old	predicate, Stream(Nat)
stutf	stut-mon	predicate, Stream(Nat)
subarray	array-copy	partial function, Array('a) × Nat × Nat → 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	natset	function, Nat × Nat → Set(Nat)
toArc	rowcol-upd	function, Matrix('a) × Nat → Array('a)
toArr	rowcol-upd	function, Matrix('a) × Nat → Array('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)
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	wolist	variable, List(Weakord)
x	list-perm	variable, List('a)
x	filter-count	variable, List('a)
x	array-as-listinstance	variable, List('a)
x	forall-indexWhere	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)
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	wolist	variable, List(Weakord)
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)
z	list-getput	variable, List('a)
z	list-del	variable, List('a)
z	olist	variable, List(Tord)
z	wolist	variable, List(Weakord)
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)
zip	filter-count	function, List('a) × List('b) → List(('a, 'b))
zip	list-as-arrayinstance	function, Array('a) × Array('b) → Array(('a, 'b))
\|	map+set	function, Map('a, 'b) × Set('a) → Map('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
∅	map	constant, Map('a, 'b)
∅	set-basic	constant, Set('a)
∅	bag-basic	constant, Bag('a)
∅	infset-basic	constant, Iset('a)
∈	map	predicate, 'a × Map('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)
∈	list-as-arrayinstance	predicate, 'a × Array('a)
∈	bag-union	predicate, 'a × Bag('a)
∈	map+set	predicate, 'b × Map('a, 'b)
∞	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
⊆	map	predicate, Map('a, 'b) × Map('a, 'b)
⊆	set-basic	predicate, Set('a) × Set('a)
⊆	infset-basic	predicate, Iset('a) × Iset('a)
⊆	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)
⊕	map+set	function, Map('a, 'b) × Map('a, 'b) → Map('a, 'b)
⌝	nat-inf	function, Nat → Natinf
⌝	stream-basic	function, Nat → 'a → Stream('a)
⌝	stream-basic	function, List('a) → Stream('a)