[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
. ( . )	list-getput	pf	List × Nat → Elem with λ x, n. n < # x
. ( . )	stream	pf	Stream × Nat → Elem with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. ( . := . )	list-getput	pf	List × Nat × Elem → List with λ x, n, a. n < # x
. ( . := . )	stream	pf	Stream × Nat × Elem → Stream with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. + .	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
. < .	nat-basic	p	Nat × Nat
. < .	list-data	p	List × List
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. ∈ .	list	p	Elem × List
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊑ .	list-last	p	List × List
. ⊑ .	stream	p	Stream × Stream
. ⊒ .	list-last	p	List × List
. butlast	list-last	pf	List → List with λ x. x ≠ []
. f	stream-basic	pf	Stream → Nat → Elem with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. 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
. 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 ≠ []
. 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
Elem	elem	s
List	list-data	s
Nat	nat-basic	s
Natinf	nat-inf	s
Stream	stream-basic	s
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
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
m	infinite-append	v	Nat
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	list-last	f	Elem × Nat → List
n	infinite-append	v	Nat
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
sublist	list-del	pf	Nat × Nat × List → List with λ n, m, x. n + m ≤ # x
tl	stream	pf	Stream → Stream with λ σ. σ ≠ []