[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 λ σ. σ ≠ []
lastnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
lastocnatstreamfnat × natstream → natinf
limnatstreampf(nat → natstream) → natstream with λ σf. mon(σf)
minnat-inffnatinf × natinf → natinf
mklistnatstreamfnat × nat → natlist
monnatstreamp(nat → natstream)
natnat-basics
natinfnat-infs
natlistnatstreams
natstreamnatstreams
posnatstreamfnat × natlist → nat
remnatstreamfnatstream × (nat → bool) → natstream
restnnatstreampfnat × natlist → natlist with λ n, x. n ≤ # x
revnatstreamfnatlist → natlist
rmdupnatstreamfnatlist → natlist
sublistnatstreampfnat × nat × natlist → natlist with λ n, m, x. n + m ≤ # x
tlnatstreampfnatstream → natstream with λ σ. σ ≠ []