[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-basic	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
. + .	nat-inf	f	natinf × natinf → natinf
. + .	stream-of-streams	f	streamlist × streamlist → streamlist
. + .	stream	f	elem × stream → stream
. + .	stream-of-streams	f	stream × streamlist → streamlist
. + .	stream	f	stream × stream → stream
. ++ .	stream-of-streams	f	streamlist × stream → streamlist
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic	f	nat → nat
. +2 .	list	f	elem × elem → list
. +l .	stream-of-streams	f	stream × stream → streamlist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	list-del	f	list × elem → list
. -1l .	stream-of-streams	f	streamlist × stream → streamlist
. -l .	list-del	f	list × elem → list
. -l .	stream-of-streams	f	streamlist × stream → streamlist
. -p .	list-del	f	list × nat → list
. -p .	stream-of-streams	f	streamlist × nat → streamlist
. .butlast	stream-of-streams	pf	streamlist → streamlist with λ σx. σx ≠ []
. .butlast	list-last	pf	list → list with λ x. x ≠ []
. .f	stream-of-streams	pf	streamstream → nat → stream with λ σσ. λ m. ∃ σf. σσ = ⌜σf⌝
. .f	stream-basic	pf	stream → nat → elem with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .head	list-data	pf	list → elem with λ x. x ≠ []
. .head	stream-of-streams	pf	streamlist → stream with λ σx. σx ≠ []
. .l	stream-of-streams	pf	streamstream → streamlist with λ σσ. finp(σσ)
. .l	stream-basic	pf	stream → list with λ σ. finp(σ)
. .last	stream-of-streams	pf	streamlist → stream with λ σx. σx ≠ []
. .last	list-last	pf	list → elem with λ x. x ≠ []
. .n	nat-inf	pf	natinf → nat with λ n∞. n∞ ≠ ∞
. .tail	list-data	pf	list → list with λ x. x ≠ []
. .tail	stream-of-streams	pf	streamlist → streamlist with λ σx. σx ≠ []
. < .	nat-basic	p	nat × nat
. < .	stream-of-streams	p	streamlist × streamlist
. < .	nat-inf	p	natinf × natinf
. < .	list-data	p	list × list
. > .	nat	p	nat × nat
. [ . ]	stream-of-streams	pf	streamstream × nat × stream → streamstream with λ σσ, n, σ. finp(σσ) → ⌜n⌝ < # σσ
. [ . ]	stream-of-streams	pf	streamstream × nat → stream with λ σσ, n. finp(σσ) → ⌜n⌝ < # σσ
. [ . ]	stream-of-streams	pf	streamlist × nat × stream → streamlist with λ σx, n, σ. n < # σx
. [ . ]	list-del	pf	list × nat → elem with λ x, n. n < # x
. [ . ]	stream-of-streams	pf	streamlist × nat → stream with λ σx, n. n < # σx
. [ . ]	list-del	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	stream	pf	stream × nat × elem → stream with λ σ1, n, a. finp(σ1) → ⌜n⌝ < # σ1
. [ . ]	stream	pf	stream × nat → elem with λ σ1, n. finp(σ1) → ⌜n⌝ < # σ1
. ∈ .	list	p	elem × list
. ∈ .	stream-of-streams	p	stream × streamlist
. ≤ .	nat	p	nat × nat
. ≤ .	stream-of-streams	p	streamstream × streamstream
. ≤ .	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-of-streams	pf	streamlist × nat → streamlist with λ σx, n. n ≤ # σx
. from .	stream	f	(nat → elem) × nat → nat → elem
. from .	stream-of-streams	pf	streamstream × nat → streamstream with λ σσ, n. finp(σσ) → ⌜n⌝ < # σσ ∨ ⌜n⌝ = # σσ
. from .	stream-of-streams	f	(nat → stream) × nat → nat → stream
. from .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. from .	stream	pf	stream × nat → stream with λ σ1, n. finp(σ1) → ⌜n⌝ < # σ1 ∨ ⌜n⌝ = # σ1
. to .	stream-of-streams	pf	streamlist × nat → streamlist with λ σx, n. n ≤ # σx
. to .	stream	f	(nat → elem) × nat → list
. to .	stream-of-streams	f	(nat → stream) × nat → streamlist
. to .	stream-of-streams	pf	streamstream × nat → streamstream with λ σσ, n. finp(σσ) → ⌜n⌝ < # σσ ∨ ⌜n⌝ = # σσ
. to .	stream	pf	stream × nat → stream with λ σ1, n. finp(σ1) → ⌜n⌝ < # σ1 ∨ ⌜n⌝ = # σ1
. to .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. to∞ .	stream-of-streams	pf	streamstream × natinf → streamstream with λ σσ, n∞. finp(σσ) → n∞ < # σσ ∨ n∞ = # σσ
. to∞ .	stream	pf	stream × natinf → stream with λ σ1, n∞. finp(σ1) → n∞ < # σ1 ∨ n∞ = # σ1
[]	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
σy	stream-of-streams	v	streamlist
σz	stream-of-streams	v	streamlist
∞	nat-inf	c	natinf
⌜ . ⌝	stream-basic	f	list → stream
⌜ . ⌝	stream-basic	f	(nat → elem) → stream
⌜ . ⌝	stream-of-streams	f	(nat → stream) → streamstream
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	stream-of-streams	f	streamlist → streamstream
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	stream-of-streams	pf	nat × streamlist → streamlist with λ n, σx. n ≤ # σx
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
c	elem	v	elem
disj	list-dup	p	list × list
disj	stream-of-streams	p	streamlist × streamlist
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	stream-of-streams	pf	nat × streamlist → streamlist with λ n, σx. n ≤ # σx
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
frome	list-del	f	list × elem → list
frome	stream-of-streams	f	streamlist × stream → streamlist
hd	stream-of-streams	pf	streamstream → stream with λ σσ. σσ ≠ []
hd	stream	pf	stream → elem with λ σ1. σ1 ≠ []
ii	infinite-append	v	nat → nat
iigen	infinite-append	v	nat → nat → nat
jj	infinite-append	v	nat → nat
lastn	stream-of-streams	pf	nat × streamlist → streamlist with λ n, σx. n ≤ # σx
lastn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
lf	infinite-append	v	nat → list
lfgen	infinite-append	v	nat → nat → list
lim	streamseq-mon-lim	pf	streamstream → stream with λ σσ. mon(σσ) ∧ σσ ≠ []
list	list-data	s
m	nat-basic	v	nat
m0	nat-inf	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-basic	v	nat
n∞	nat-inf	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
natinf	nat-inf	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	pf	nat × streamlist → streamlist with λ n, σx. n ≤ # σx
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
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	stream-of-streams	pf	nat × nat × streamlist → streamlist with λ n, m, σx. n + m ≤ # σx
sublist	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
tl	stream-of-streams	pf	streamstream → streamstream with λ σσ. σσ ≠ []
tl	stream	pf	stream → stream with λ σ1. σ1 ≠ []
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
y	list-data	v	list
z	list-data	v	list