[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	f	stream → natinf
# .	list-data	f	list → nat
. '	list	f	elem → list
. + .	nat-basic	f	nat × nat → nat
. + .	stream	f	stream × stream → stream
. + .	list-data	f	elem × list → list
. + .	stream	f	elem × stream → stream
. + .	list	f	list × list → list
. + .	nat-inf	f	natinf × natinf → natinf
. + .	list	f	list × elem → list
. ++ .	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
. < .	nat-inf	p	natinf × natinf
. < .	list-data	p	list × list
. > .	nat	p	nat × nat
. [ . ]	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-del	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	list-del	pf	list × nat → elem with λ x, n. n < # x
. ∈ .	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	pf	list × nat → list with λ x, n. n ≤ # x
. from .	stream	f	(nat → elem) × nat → nat → elem
. from .	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	f	(nat → elem) × nat → list
. to .	stream	pf	stream × nat → stream with λ σ1, n. finp(σ1) → ⌜n⌝ < # σ1 ∨ ⌜n⌝ = # σ1
. to∞ .	stream	pf	stream × natinf → stream with λ σ1, n∞. finp(σ1) → n∞ < # σ1 ∨ n∞ = # σ1
[]	list-data	c	list
[]	stream	c	stream
σ	stream-basic	v	stream
σ1	stream	v	stream
σ2	stream	v	stream
∞	nat-inf	c	natinf
⌜ . ⌝	stream-basic	f	list → stream
⌜ . ⌝	stream-basic	f	(nat → elem) → stream
⌜ . ⌝	nat-inf	f	nat → natinf
a	elem	v	elem
a0	list-data	v	elem
b	elem	v	elem
butlastn	list-last	pf	nat × list → list with λ n, x. n ≤ # x
c	elem	v	elem
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 λ σ1. σ1 ≠ []
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	nat-basic	v	nat
m0	nat-inf	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	list-last	f	elem × nat → list
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
nextli	inf-app-list	v	list → list
nextnli	inf-app-list	v	list × nat → 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
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 λ σ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