[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
# .	list-data	f	list → nat
# .	stream	f	stream → natinf
# .	stream-of-streams	f	streamlist → nat
# .	stream-of-streams	f	streamstream → natinf
. '	list	f	elem → list
. '	stream-of-streams	f	stream → streamlist
. + .	nat-basic	f	nat × nat → nat
. + .	list-data	f	elem × list → list
. + .	list	f	list × list → list
. + .	list	f	list × elem → list
. + .	nat-inf	f	natinf × natinf → natinf
. + .	stream	f	elem × stream → stream
. + .	stream	f	stream × stream → stream
. + .	stream-of-streams	f	stream × streamlist → streamlist
. + .	stream-of-streams	f	streamlist × streamlist → streamlist
. + .	stream-of-streams	f	streamlist × stream → streamlist
. + .	stream-of-streams	f	stream × streamstream → streamstream
. + .	stream-of-streams	f	streamstream × streamstream → streamstream
. ++ .	list-dup	f	list × elem → list
. ++ .	stream-of-streams	f	streamlist × stream → streamlist
. +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	list-last	pf	list → list with λ x. x ≠ []
. .butlast	stream-of-streams	pf	streamlist → streamlist with λ x. x ≠ []
. .f	stream-basic	pf	stream → nat → elem with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .f	stream-of-streams	pf	streamstream → nat → stream 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-basic	pf	stream → list with λ σ. finp(σ)
. .l	stream-of-streams	pf	streamstream → streamlist with λ σ. finp(σ)
. .last	list-last	pf	list → elem with λ x. x ≠ []
. .last	stream-of-streams	pf	streamlist → stream 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
. < .	list-data	p	list × list
. < .	nat-inf	p	natinf × natinf
. < .	stream-of-streams	p	streamlist × streamlist
. > .	nat	p	nat × nat
. [ . ]	list-getput	pf	list × nat → elem with λ x, n. n < # x
. [ . ]	list-getput	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	stream	pf	stream × nat → elem with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	stream	pf	stream × nat × elem → stream with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. [ . ]	stream-of-streams	pf	streamlist × nat → stream with λ x, n. n < # x
. [ . ]	stream-of-streams	pf	streamlist × nat × stream → streamlist with λ x, n, a. n < # x
. [ . ]	stream-of-streams	pf	streamstream × nat → stream with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	stream-of-streams	pf	streamstream × nat × stream → streamstream with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. ∈ .	list	p	elem × list
. ∈ .	stream-of-streams	p	stream × streamlist
. ≤ .	nat	p	nat × nat
. ≤ .	stream	p	stream × stream
. ≤ .	stream-of-streams	p	streamstream × streamstream
. ≥ .	nat	p	nat × nat
. ⊑ .	list-last	p	list × list
. ⊑ .	stream-of-streams	p	streamlist × streamlist
. ⊒ .	list-last	p	list × list
. ⊒ .	stream-of-streams	p	streamlist × streamlist
. from .	stream	f	(nat → elem) × nat → nat → elem
. from .	stream-of-streams	f	(nat → stream) × nat → nat → stream
. from .	stream	pf	stream × nat → stream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. from .	stream-of-streams	pf	streamstream × nat → streamstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	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	pf	stream × nat → stream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. to .	stream-of-streams	pf	streamstream × nat → streamstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	stream-of-streams	pf	streamlist × nat → streamlist with λ x, n. n ≤ # x
. to∞ .	stream	pf	stream × natinf → stream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
. to∞ .	stream-of-streams	pf	streamstream × natinf → streamstream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]	list-data	c	list
[]	stream	c	stream
[]	stream-of-streams	c	streamlist
[]	stream-of-streams	c	streamstream
∞	nat-inf	c	natinf
⌜ . ⌝	stream-basic	f	list → stream
⌜ . ⌝	stream-basic	f	(nat → elem) → stream
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	stream-of-streams	f	streamlist → streamstream
⌜ . ⌝	stream-of-streams	f	(nat → stream) → streamstream
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
butlastn	stream-of-streams	pf	nat × streamlist → streamlist with λ n, x. n ≤ # x
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-basic	p	stream
finp	stream-of-streams	p	streamstream
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
firstn	stream-of-streams	pf	nat × streamlist → streamlist with λ n, x. n ≤ # x
frome	list-del	f	list × elem → list
frome	stream-of-streams	f	streamlist × stream → streamlist
hd	stream	pf	stream → elem with λ σ. σ ≠ []
hd	stream-of-streams	pf	streamstream → stream with λ σ. σ ≠ []
lastn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
lastn	stream-of-streams	pf	nat × streamlist → streamlist with λ n, x. n ≤ # x
list	list-data	s
min	nat-inf	f	natinf × natinf → natinf
mklist	list-last	f	elem × nat → list
mklist	stream-of-streams	f	stream × nat → streamlist
nat	nat-basic	s
natinf	nat-inf	s
pos	list-del	f	elem × list → nat
pos	stream-of-streams	f	stream × streamlist → nat
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
restn	stream-of-streams	pf	nat × streamlist → streamlist 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	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
sublist	stream-of-streams	pf	nat × nat × streamlist → streamlist with λ n, m, x. n + m ≤ # x
tl	stream	pf	stream → stream with λ σ. σ ≠ []
tl	stream-of-streams	pf	streamstream → streamstream with λ σ. σ ≠ []