[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
# .	indexseq	f	ilist → nat
# .	indexseq	f	illist → nat
#oc	indexseq	f	nat × ilist → nat
. '	indexseq	f	ilist → illist
. '	indexseq	f	nat → ilist
. + .	nat-basic2	f	nat × nat → nat
. + .	indexseq	f	illist × ilist → illist
. + .	indexseq	f	nat × ilist → ilist
. + .	indexseq	f	illist × illist → illist
. + .	indexseq	f	ilist × ilist → ilist
. + .	indexseq	f	ilist × illist → illist
. + .	indexseq	f	ilist × nat → ilist
. ++ .	indexseq	f	illist × ilist → illist
. ++ .	indexseq	f	ilist × nat → ilist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	indexseq	f	illist × nat → illist
. -1l .	indexseq	f	illist × ilist → illist
. -1l .	indexseq	f	ilist × nat → ilist
. -1p .	indexseq	f	ilist × nat → ilist
. -l .	indexseq	f	ilist × nat → ilist
. -l .	indexseq	f	illist × ilist → illist
. .butlast	indexseq	f	ilist → ilist
. .butlast	indexseq	f	illist → illist
. .first	indexseq	f	ilist → nat
. .first	indexseq	f	illist → ilist
. .last	indexseq	f	illist → ilist
. .last	indexseq	f	ilist → nat
. .rest	indexseq	f	ilist → ilist
. .rest	indexseq	f	illist → illist
. < .	indexseq	p	illist × illist
. < .	indexseq	p	ilist × ilist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	indexseq	f	ilist × nat → nat
. [ . ]	indexseq	f	illist × nat × ilist → illist
. [ . ]	indexseq	f	ilist × nat × nat → ilist
. [ . ]	indexseq	f	illist × nat → ilist
. \ .	indexseq	f	ilist × ilist → ilist
. ∈ .	indexseq	p	ilist × illist
. ∈ .	indexseq	p	nat × ilist
. ∪ .	indexseq	f	ilist × ilist → ilist
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	indexseq	p	ilist × ilist
. ⊆m .	indexseq	p	ilist × ilist
. ⊑ .	indexseq	p	illist × illist
. ⊑ .	indexseq	p	ilist × ilist
. ⊒ .	indexseq	p	illist × illist
. ⊒ .	indexseq	p	ilist × ilist
. plus .	indexseq	f	nat × nat → ilist
. plus .	indexseq	f	ilist × ilist → illist
[]	indexseq	c	ilist
[]	indexseq	c	illist
butlastn	indexseq	f	nat × illist → illist
butlastn	indexseq	f	nat × ilist → ilist
disj	indexseq	p	illist × illist
disj	indexseq	p	ilist × ilist
dups	indexseq	p	illist
dups	indexseq	p	ilist
fillfirst	indexseq	f	nat × nat × ilist → ilist
fillfirst	indexseq	f	nat × ilist × illist → illist
filter	indexseq	f	ilist × ilist → ilist
firstn	indexseq	f	nat × ilist → ilist
firstn	indexseq	f	nat × illist → illist
frome	indexseq	f	illist × ilist → illist
frome	indexseq	f	ilist × nat → ilist
ilist	indexseq	s
illist	indexseq	s
ins≤	indexseq	f	nat × ilist → ilist
ix	indexseq	v	ilist
ix0	indexseq	v	ilist
ix1	indexseq	v	ilist
ix10	indexseq	v	ilist
ix2	indexseq	v	ilist
ix3	indexseq	v	ilist
ix4	indexseq	v	ilist
ix5	indexseq	v	ilist
ix6	indexseq	v	ilist
ix7	indexseq	v	ilist
ix8	indexseq	v	ilist
ix9	indexseq	v	ilist
ixs	indexseq	v	illist
ixs0	indexseq	v	illist
ixs1	indexseq	v	illist
ixs10	indexseq	v	illist
ixs2	indexseq	v	illist
ixs3	indexseq	v	illist
ixs4	indexseq	v	illist
ixs5	indexseq	v	illist
ixs6	indexseq	v	illist
ixs7	indexseq	v	illist
ixs8	indexseq	v	illist
ixs9	indexseq	v	illist
lastn	indexseq	f	nat × ilist → ilist
lastn	indexseq	f	nat × illist → illist
m	nat-basic2	v	nat
merge	indexseq	f	ilist × ilist → ilist
mklist	indexseq	f	nat × nat → ilist
mklist	indexseq	f	ilist × nat → illist
n	nat-basic1	v	nat
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
n3	indexseq	v	nat
n4	indexseq	v	nat
n5	indexseq	v	nat
n6	indexseq	v	nat
nat	nat-basic1	s
ordered<	indexseq	p	ilist
ordered≤	indexseq	p	ilist
perm	indexseq	p	ilist × ilist
pos	indexseq	f	nat × ilist → nat
pos	indexseq	f	ilist × illist → nat
restn	indexseq	f	nat × illist → illist
restn	indexseq	f	nat × ilist → ilist
rev	indexseq	f	ilist → ilist
rev	indexseq	f	illist → illist
rmdup	indexseq	f	ilist → ilist
rmdup	indexseq	f	illist → illist
sublist	indexseq	f	nat × nat × illist → illist
sublist	indexseq	f	nat × nat × ilist → ilist