[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
. '	list	f	elem → list
. + .	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
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic	f	nat → nat
. +2 .	list	f	elem × elem → list
. - .	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
. -l .	list-del	f	list × elem → list
. -p .	list-del	f	list × nat → list
. .butlast	list-last	pf	list → list with λ x. x ≠ []
. .f	stream-basic	pf	stream → nat → elem with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .head	list-data	pf	list → elem with λ x. x ≠ []
. .l	stream-basic	pf	stream → list with λ σ. finp(σ)
. .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 ≠ []
. < .	nat-basic	p	nat × nat
. < .	list-data	p	list × list
. < .	nat-inf	p	natinf × natinf
. > .	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⌝ < # σ
. ∈ .	list	p	elem × list
. ≤ .	nat	p	nat × nat
. ≤ .	stream	p	stream × stream
. ≥ .	nat	p	nat × nat
. ⊑ .	list-last	p	list × list
. ⊒ .	list-last	p	list × list
. from .	stream	f	(nat → elem) × nat → nat → elem
. from .	stream	pf	stream × nat → stream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. to .	stream	f	(nat → elem) × nat → list
. to .	stream	pf	stream × nat → stream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	stream	pf	list × nat → list with λ x, n. n ≤ # x
. to∞ .	stream	pf	stream × natinf → stream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]	list-data	c	list
[]	stream	c	stream
σ	infinite-append	v	stream
∞	nat-inf	c	natinf
⌜ . ⌝	stream-basic	f	list → stream
⌜ . ⌝	stream-basic	f	(nat → elem) → stream
⌜ . ⌝	nat-inf	f	nat → natinf
a	infinite-append	v	elem
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
disj	list-dup	p	list × list
dups	list-dup	p	list
elem	elem	s
fillfirst	list-last	f	nat × elem × list → list
finp	stream-basic	p	stream
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
frome	list-del	f	list × elem → list
hd	stream	pf	stream → elem with λ σ. σ ≠ []
ii	infinite-append	v	nat → nat
iigen	infinite-append	v	nat → nat → nat
jj	infinite-append	v	nat → nat
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
list	list-data	s
m	infinite-append	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	list-last	f	elem × nat → list
n	infinite-append	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	infinite-append	v	nat → elem
nfgen	infinite-append	v	nat → nat → elem
pos	list-del	f	elem × list → nat
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
rev	list-last	f	list → list
rmdup	list-dup	f	list → list
stream	stream-basic	s
sublist	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
tl	stream	pf	stream → stream with λ σ. σ ≠ []