[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
# .natstreamfnatlist → nat
# .natstreamfnatstream → natinf
. 'natstreamfnat → natlist
. + .nat-basicfnat × nat → nat
. + .natstreamfnat × natlist → natlist
. + .natstreamfnatlist × natlist → natlist
. + .natstreamfnatlist × nat → natlist
. + .nat-inffnatinf × natinf → natinf
. + .natstreamfnat × natstream → natstream
. + .natstreamfnatstream × natstream → natstream
. ++ .natstreamfnatlist × nat → natlist
. +1nat-basicfnat → nat
. +l .natstreamfnat × nat → natlist
. - .natpfnat × nat → nat with λ n, m. n ≥ m
. -1nat-basicpfnat → nat with λ n. n ≠ 0
. -1l .natstreamfnatlist × nat → natlist
. -l .natstreamfnatlist × nat → natlist
. -pos .natstreamfnatlist × nat → natlist
. .butlastnatstreampfnatlist → natlist with λ x. x ≠ []
. .fnatstreampfnatstream → nat → nat with λ σ. λ m. ∃ nf. σ = ⌜nf⌝
. .headnatstreampfnatlist → nat with λ x. x ≠ []
. .lnatstreampfnatstream → natlist with λ σ. finp(σ)
. .lastnatstreampfnatlist → nat with λ x. x ≠ []
. .nnat-infpfnatinf → nat with λ n∞. n∞ ≠ ∞
. .tailnatstreampfnatlist → natlist with λ x. x ≠ []
. < .nat-basicpnat × nat
. < .natstreampnatlist × natlist
. < .nat-infpnatinf × natinf
. > .natpnat × nat
. [ . ]natstreampfnatlist × nat → nat with λ x, n. n < # x
. [ . ]natstreampfnatlist × nat × nat → natlist with λ x, n, a. n < # x
. [ . ]natstreampfnatstream × nat → nat with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]natstreampfnatstream × nat × nat → natstream with λ σ, n, a. finp(σ) → ⌜n⌝ < # σ
. ∈ .natstreampnat × natlist
. ≤ .natpnat × nat
. ≤ .natstreampnatstream × natstream
. ≥ .natpnat × nat
. ⊑ .natstreampnatlist × natlist
. ⊑ .natstreampnatstream × natstream
. ⊒ .natstreampnatlist × natlist
. from .natstreamf(nat → nat) × nat → nat → nat
. from .natstreampfnatstream × nat → natstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .natstreampfnatlist × nat → natlist with λ x, n. n ≤ # x
. to .natstreamf(nat → nat) × nat → natlist
. to .natstreampfnatstream × nat → natstream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .natstreampfnatlist × nat → natlist with λ x, n. n ≤ # x
. to∞ .natstreampfnatstream × natinf → natstream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]natstreamcnatlist
[]natstreamcnatstream
∞nat-infcnatinf
⌜ . ⌝natstreamfnatlist → natstream
⌜ . ⌝natstreamf(nat → nat) → natstream
⌜ . ⌝nat-inffnat → natinf
butlastnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
cntnatstreamfnat × natstream → natinf
disjnatstreampnatlist × natlist
dupsnatstreampnatlist
fillfirstnatstreamfnat × nat × natlist → natlist
filternatstreamf(nat → bool) × natstream → natstream
finpnatstreampnatstream
firstnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
fromenatstreamfnatlist × nat → natlist
hdnatstreampfnatstream → nat with λ σ. σ ≠ []
invstut-monpfnatstream → natstream with λ nσ. stutf(nσ)
lastnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
lastocnatstreamfnat × natstream → natinf
leninvstut-monfnatstream → natinf
limnatstreampf(nat → natstream) → natstream with λ σf. mon(σf)
max∞stut-monf(nat → bool) → natinf
minnat-inffnatinf × natinf → natinf
minstut-monpfnatstream × nat → nat with λ nσ, n. mon<(nσ)
mklistnatstreamfnat × nat → natlist
monnatstreamp(nat → natstream)
mon<stut-monpnatstream
mon≤stut-monpnatstream
nstut-monvnat
nσstut-monvnatstream
natnat-basics
natinfnat-infs
natlistnatstreams
natstreamnatstreams
nlstut-monvnatlist
nnfstut-monvnat → nat
npstut-monvnat → bool
posnatstreamfnat × natlist → nat
remnatstreamfnatstream × (nat → bool) → natstream
restnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
revnatstreamfnatlist → natlist
rmdupnatstreamfnatlist → natlist
stutfstut-monpnatstream
sublistnatstreampfnat × nat × natlist → natlist with λ n, m, x. n + m ≤ # x
tlnatstreampfnatstream → natstream with λ σ. σ ≠ []