[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
# .	stream-of-streams	f	streamstream → natinf
# .	list-data	f	list → nat
# .	stream-of-streams	f	streamlist → nat
# .	stream	f	stream → natinf
. '	stream-of-streams	f	stream → streamlist
. '	list	f	elem → list
. + .	nat-basic2	f	nat × nat → nat
. + .	stream-of-streams	f	streamstream × streamstream → streamstream
. + .	list-data	f	elem × list → list
. + .	stream-of-streams	f	stream × streamstream → streamstream
. + .	list	f	list × list → list
. + .	list	f	list × elem → list
. + .	stream-of-streams	f	streamlist × stream → streamlist
. + .	list	f	elem × elem → list
. + .	stream-of-streams	f	streamlist × streamlist → streamlist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	stream-of-streams	f	stream × streamlist → streamlist
. + .	stream	f	elem × stream → stream
. + .	stream	f	stream × stream → stream
. ++ .	stream-of-streams	f	streamlist × stream → streamlist
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic1	f	nat → nat
. +l .	stream-of-streams	f	stream × stream → streamlist
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	stream-of-streams	f	streamlist × nat → streamlist
. -1l .	stream-of-streams	f	streamlist × stream → streamlist
. -1l .	list-del	f	list × elem → list
. -1l .	list-del	f	list × nat → list
. -l .	list-del	f	list × elem → list
. -l .	stream-of-streams	f	streamlist × stream → streamlist
. .butlast	list-last	f	list → list
. .butlast	stream-of-streams	f	streamlist → streamlist
. .f	stream-of-streams	f	streamstream → nat → stream
. .f	stream-basic	f	stream → nat → elem
. .first	list-data	f	list → elem
. .first	stream-of-streams	f	streamlist → stream
. .l	stream-of-streams	f	streamstream → streamlist
. .l	stream-basic	f	stream → list
. .last	list-last	f	list → elem
. .last	stream-of-streams	f	streamlist → stream
. .n	nat-inf-basic	f	natinf → nat
. .rest	list-data	f	list → list
. .rest	stream-of-streams	f	streamlist → streamlist
. < .	stream-of-streams	p	streamlist × streamlist
. < .	nat-inf	p	natinf × natinf
. < .	nat-basic1	p	nat × nat
. < .	list-data	p	list × list
. > .	nat	p	nat × nat
. [ . ]	list-del	f	list × nat → elem
. [ . ]	stream-of-streams	f	streamstream × nat × stream → streamstream
. [ . ]	list-del	f	list × nat × elem → list
. [ . ]	stream-of-streams	f	streamstream × nat → stream
. [ . ]	stream	f	stream × nat → elem
. [ . ]	stream-of-streams	f	streamlist × nat × stream → streamlist
. [ . ]	stream	f	stream × nat × elem → stream
. [ . ]	stream-of-streams	f	streamlist × nat → stream
. ∈ .	stream-of-streams	p	stream × streamlist
. ∈ .	list	p	elem × list
. ≤ .	stream-of-streams	p	streamstream × streamstream
. ≤ .	nat	p	nat × nat
. ≤ .	stream	p	stream × stream
. ≥ .	nat	p	nat × nat
. ⊑ .	streamseq-mon-lim	p	stream × stream
. ⊑ .	list-last	p	list × list
. ⊑ .	stream-of-streams	p	streamlist × streamlist
. ⊒ .	stream-of-streams	p	streamlist × streamlist
. ⊒ .	list-last	p	list × list
. from .	stream	f	stream × nat → stream
. from .	stream-of-streams	f	(nat → stream) × nat → nat → stream
. from .	stream	f	list × nat → list
. from .	stream-of-streams	f	streamlist × nat → streamlist
. from .	stream	f	(nat → elem) × nat → nat → elem
. from .	stream-of-streams	f	streamstream × nat → streamstream
. to .	stream	f	stream × nat → stream
. to .	stream-of-streams	f	(nat → stream) × nat → streamlist
. to .	stream-of-streams	f	streamlist × nat → streamlist
. to .	stream	f	list × nat → list
. to .	stream-of-streams	f	streamstream × nat → streamstream
. to .	stream	f	(nat → elem) × nat → list
. to∞ .	stream	f	stream × natinf → stream
. to∞ .	stream-of-streams	f	streamstream × natinf → streamstream
[]	list-data	c	list
[]	stream	c	stream
[]	stream-of-streams	c	streamlist
[]	stream-of-streams	c	streamstream
σ	stream-basic	v	stream
σσ	stream-of-streams	v	streamstream
σσ1	stream-of-streams	v	streamstream
σσ2	stream-of-streams	v	streamstream
σ0	stream-of-streams	v	stream
σ1	stream	v	stream
σ2	stream	v	stream
σf	stream-of-streams	v	nat → stream
σf0	stream-of-streams	v	nat → stream
σx	stream-of-streams	v	streamlist
σx0	stream-of-streams	v	streamlist
σx1	stream-of-streams	v	streamlist
σx2	stream-of-streams	v	streamlist
σy	stream-of-streams	v	streamlist
σy0	stream-of-streams	v	streamlist
σy1	stream-of-streams	v	streamlist
σy2	stream-of-streams	v	streamlist
σz	stream-of-streams	v	streamlist
σz0	stream-of-streams	v	streamlist
σz1	stream-of-streams	v	streamlist
σz2	stream-of-streams	v	streamlist
∞	nat-inf-basic	c	natinf
⌜ . ⌝	stream-basic	f	list → stream
⌜ . ⌝	stream-basic	f	(nat → elem) → stream
⌜ . ⌝	stream-of-streams	f	(nat → stream) → streamstream
⌜ . ⌝	nat-inf-basic	f	nat → natinf
⌜ . ⌝	stream-of-streams	f	streamlist → streamstream
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	list-last	f	nat × list → list
butlastn	stream-of-streams	f	nat × streamlist → streamlist
c	elem	v	elem
disj	stream-of-streams	p	streamlist × streamlist
disj	list-dup	p	list × list
dups	list-dup	p	list
dups	stream-of-streams	p	streamlist
elem	elem	s
fillfirst	list-last	f	nat × elem × list → list
fillfirst	stream-of-streams	f	nat × stream × streamlist → streamlist
finp	stream-of-streams	p	streamstream
finp	stream-basic	p	stream
firstn	list-del	f	nat × list → list
firstn	stream-of-streams	f	nat × streamlist → streamlist
frome	list-del	f	list × elem → list
frome	stream-of-streams	f	streamlist × stream → streamlist
hd	stream-of-streams	f	streamstream → stream
hd	stream	f	stream → elem
ii	infinite-append	v	nat → nat
iigen	infinite-append	v	nat → nat → nat
jj	infinite-append	v	nat → nat
lastn	list-del	f	nat × list → list
lastn	stream-of-streams	f	nat × streamlist → streamlist
lf	infinite-append	v	nat → list
lfgen	infinite-append	v	nat → nat → list
lim	streamseq-mon-lim	f	streamstream → stream
list	list-data	s
m	nat-basic1	v	nat
m0	nat-inf-basic	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	list-last	f	elem × nat → list
mklist	stream-of-streams	f	stream × nat → streamlist
mon	streamseq-mon-lim	p	streamstream
n	nat-basic1	v	nat
n∞	nat-inf-basic	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
natinf	nat-inf-basic	s
nextj	infinite-append	v	nat × elem → nat
nextl	infinite-append	v	nat × elem → list
nf	stream-basic	v	nat → elem
nf0	stream-basic	v	nat → elem
nfgen	infinite-append	v	nat → nat → elem
pos	list-del	f	elem × list → nat
pos	stream-of-streams	f	stream × streamlist → nat
restn	stream-of-streams	f	nat × streamlist → streamlist
restn	list-del	f	nat × list → list
rev	list-last	f	list → list
rev	stream-of-streams	f	streamlist → streamlist
rmdup	list-dup	f	list → list
rmdup	stream-of-streams	f	streamlist → streamlist
stream	stream-basic	s
streamlist	stream-of-streams	s
streamstream	stream-of-streams	s
sublist	list-del	f	nat × nat × list → list
sublist	stream-of-streams	f	nat × nat × streamlist → streamlist
tl	stream	f	stream → stream
tl	stream-of-streams	f	streamstream → streamstream
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
x2	list-data	v	list
y	list-data	v	list
y0	list-data	v	list
y1	list-data	v	list
y2	list-data	v	list
z	list-data	v	list
z0	list-data	v	list
z1	list-data	v	list
z2	list-data	v	list