[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
# .	natstream	f	Natlist → Nat
# .	natstream	f	Natstream → Natinf
. '	natstream	f	Nat → Natlist
. ( . )	natstream	pf	Natlist × Nat → Nat with λ x, n. n < # x
. ( . )	natstream	pf	Natstream × Nat → Nat with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. ( . := . )	natstream	pf	Natlist × Nat × Nat → Natlist with λ x, n, a. n < # x
. ( . := . )	natstream	pf	Natstream × Nat × Nat → Natstream with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. + .	nat-basic	f	Nat × Nat → Nat
. + .	natstream	f	Nat × Natlist → Natlist
. + .	natstream	f	Natlist × Natlist → Natlist
. + .	natstream	f	Natlist × Nat → Natlist
. + .	nat-inf	f	Natinf × Natinf → Natinf
. + .	natstream	f	Nat × Natstream → Natstream
. + .	natstream	f	Natstream × Natstream → Natstream
. ++ .	natstream	f	Natlist × Nat → Natlist
. +1	nat-basic	f	Nat → Nat
. +l .	natstream	f	Nat × Nat → Natlist
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	natstream	f	Natlist × Nat → Natlist
. -l .	natstream	f	Natlist × Nat → Natlist
. -pos .	natstream	f	Natlist × Nat → Natlist
. < .	nat-basic	p	Nat × Nat
. < .	natstream	p	Natlist × Natlist
. < .	nat-inf	p	Natinf × Natinf
. > .	nat	p	Nat × Nat
. ∈ .	natstream	p	Nat × Natlist
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊑ .	natstream	p	Natlist × Natlist
. ⊑ .	natstream	p	Natstream × Natstream
. ⊒ .	natstream	p	Natlist × Natlist
. butlast	natstream	pf	Natlist → Natlist with λ x. x ≠ []
. f	natstream	pf	Natstream → Nat → Nat with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. from .	natstream	f	(Nat → Nat) × Nat → Nat → Nat
. from .	natstream	pf	Natstream × Nat → Natstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	natstream	pf	Natlist × Nat → Natlist with λ x, n. n ≤ # x
. head	natstream	pf	Natlist → Nat with λ x. x ≠ []
. l	natstream	pf	Natstream → Natlist with λ σ. finp(σ)
. last	natstream	pf	Natlist → Nat with λ x. x ≠ []
. n	nat-inf	pf	Natinf → Nat with λ n∞. n∞ ≠ ∞
. tail	natstream	pf	Natlist → Natlist with λ x. x ≠ []
. to .	natstream	f	(Nat → Nat) × Nat → Natlist
. to .	natstream	pf	Natstream × Nat → Natstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	natstream	pf	Natlist × Nat → Natlist with λ x, n. n ≤ # x
. to∞ .	natstream	pf	Natstream × Natinf → Natstream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]	natstream	c	Natlist
[]	natstream	c	Natstream
∞	nat-inf	c	Natinf
⌜ . ⌝	natstream	f	Natlist → Natstream
⌜ . ⌝	natstream	f	(Nat → Nat) → Natstream
⌜ . ⌝	nat-inf	f	Nat → Natinf
Nat	nat-basic	s
Natinf	nat-inf	s
Natlist	natstream	s
Natstream	natstream	s
butlastn	natstream	pf	Nat × Natlist → Natlist with λ n, x. n ≤ # x
cnt	natstream	f	Nat × Natstream → Natinf
disj	natstream	p	Natlist × Natlist
dups	natstream	p	Natlist
fillfirst	natstream	f	Nat × Nat × Natlist → Natlist
filter	natstream	f	(Nat → Bool) × Natstream → Natstream
finp	natstream	p	Natstream
firstn	natstream	pf	Nat × Natlist → Natlist with λ n, x. n ≤ # x
frome	natstream	f	Natlist × Nat → Natlist
hd	natstream	pf	Natstream → Nat with λ σ. σ ≠ []
lastn	natstream	pf	Nat × Natlist → Natlist with λ n, x. n ≤ # x
lastoc	natstream	f	Nat × Natstream → Natinf
lim	natstream	pf	(Nat → Natstream) → Natstream with λ σf. mon(σf)
min	nat-inf	f	Natinf × Natinf → Natinf
mklist	natstream	f	Nat × Nat → Natlist
mon	natstream	p	(Nat → Natstream)
pos	natstream	f	Nat × Natlist → Nat
rem	natstream	f	Natstream × (Nat → Bool) → Natstream
restn	natstream	pf	Nat × Natlist → Natlist with λ n, x. n ≤ # x
rev	natstream	f	Natlist → Natlist
rmdup	natstream	f	Natlist → Natlist
sublist	natstream	pf	Nat × Nat × Natlist → Natlist with λ n, m, x. n + m ≤ # x
tl	natstream	pf	Natstream → Natstream with λ σ. σ ≠ []