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

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	natlista	f	natset → nat
# .	natlista	f	natlist → nat
#oc	natlista	f	nat × natlist → nat
. % .	int-div	f	int × int → int
. % .	nat-div	f	nat × nat → nat
. '	natlista	f	nat → natlist
. * .	int-mult	f	int × int → int
. * .	nat-mult	f	nat × nat → nat
. + .	int-basic2	f	int × int → int
. + .	nat-basic2	f	nat × nat → nat
. + .	natlista	f	natlist × nat → natlist
. + .	natlista	f	nat × natlist → natlist
. + .	natlista	f	natlist × natlist → natlist
. ++ .	natlista	f	natset × nat → natset
. ++ .	natlista	f	natlist × nat → natlist
. +1	int-basic1	f	int → int
. +1	nat-basic1	f	nat → nat
. +l .	natlista	f	nat × nat → natlist
. - .	int-abs	f	int × int → int
. - .	nat	f	nat × nat → nat
. -- .	natlista	f	natset × nat → natset
. -1	int-basic1	f	int → int
. -1	nat-basic1	f	nat → nat
. -1l .	natlista	f	natlist × nat → natlist
. -l .	natlista	f	natlist × nat → natlist
. -pos .	natlista	f	natlist × nat → natlist
. .butlast	natlista	f	natlist → natlist
. .butmax	natlista	f	natset → natset
. .butmin	natlista	f	natset → natset
. .first	natlista	f	natlist → nat
. .last	natlista	f	natlist → nat
. .max	natlista	f	natset → nat
. .min	natlista	f	natset → nat
. .rest	natlista	f	natlist → natlist
. / .	int-div	f	int × int → int
. / .	nat-div	f	nat × nat → nat
. < .	natlista	p	natset × nat
. < .	natlista	p	nat × natset
. < .	int-basic1	p	int × int
. < .	natlista	p	natlist × natlist
. < .	nat-basic1	p	nat × nat
. > .	int-abs	p	int × int
. > .	nat	p	nat × nat
. [ . ]	natlista	f	natlist × nat → nat
. [ . ]	natlista	f	natlist × nat × nat → natlist
. \ .	natlista	f	natlist × natlist → natlist
. \ .	natlista	f	natset × natset → natset
. ∈ .	natlista	p	nat × natset
. ∈ .	natlista	p	nat × natlist
. ∩ .	natlista	f	natset × natset → natset
. ∪ .	natlista	f	natlist × natlist → natlist
. ∪ .	natlista	f	natset × natset → natset
. ≤ .	nat	p	nat × nat
. ≤ .	int-abs	p	int × int
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
. ⊆ .	natlista	p	natset × natset
. ⊆ .	natlista	p	natlist × natlist
. ⊆m .	natlista	p	natlist × natlist
. ⊑ .	natlista	p	natlist × natlist
. ⊒ .	natlista	p	natlist × natlist
[]	natlista	c	natlist
{ . }	natlista	f	nat → natset
~ .	int-abs	f	int → int
Π .	natlist	f	natlist → nat
Σ .	natlist	f	natlist → nat
∅	natlista	c	natset
abs	int-abs	f	int → int
butlastn	natlista	f	nat × natlist → natlist
disj	natlista	p	natlist × natlist
dups	natlista	p	natlist
fillfirst	natlista	f	nat × nat × natlist → natlist
filter	natlista	f	natlist × natlist → natlist
firstn	natlista	f	nat × natlist → natlist
frome	natlista	f	natlist × nat → natlist
i	int-basic1	v	int
i→n	intnat	f	int → nat
i0	int-basic1	v	int
ins≤	natlista	f	nat × natlist → natlist
int	int-basic1	s
j	int-basic1	v	int
j0	int-basic1	v	int
lastn	natlista	f	nat × natlist → natlist
list2set	natlista	f	natlist → natset
m	nat-basic1	v	nat
m0	natlista	v	nat
m1	natlista	v	nat
m2	natlista	v	nat
m3	natlista	v	nat
merge	natlista	f	natlist × natlist → natlist
mklist	natlista	f	nat × nat → natlist
n	nat-basic1	v	nat
n→i	intnat	f	nat → int
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
natlist	natlista	s
nats	natlista	v	natlist
nats0	natlista	v	natlist
nats1	natlista	v	natlist
nats10	natlista	v	natlist
nats2	natlista	v	natlist
nats3	natlista	v	natlist
nats4	natlista	v	natlist
nats5	natlista	v	natlist
nats6	natlista	v	natlist
nats7	natlista	v	natlist
nats8	natlista	v	natlist
nats9	natlista	v	natlist
natset	natlista	s
natset	natlista	v	natset
natset0	natlista	v	natset
natset1	natlista	v	natset
natset2	natlista	v	natset
ordered<	natlista	p	natlist
ordered≤	natlista	p	natlist
perm	natlista	p	natlist × natlist
pos	natlista	f	nat × natlist → nat
restn	natlista	f	nat × natlist → natlist
rev	natlista	f	natlist → natlist
rmdup	natlista	f	natlist → natlist
set2list	natlista	f	natset → natlist
sublist	natlista	f	nat × nat × natlist → natlist