[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,
enrich
natstream
with
functions max∞ : (nat → bool) → natinf;
min : natstream × nat → nat;
comment: defined for nonempty streams only.;
inv : natstream → natstream;
comment: inverse of a stuttering stream (strict monotonic).;
rinv : natstream → nat → nat;
comment: inverse of a strict monotonic stream (stutters).;
leninv : natstream → natinf;
comment: length of the inverse of a stuttering stream.;
predicates stutf : natstream;
mon≤ : natstream;
mon< : natstream;
variables np : nat → bool;
nσ0 : natstream;
axioms maxinf-def
: ⊦ (max∞(np) = ∞ ⊃ (∀ n. ∃ n0. n < n0 ∧ np(n0)) ∨ (∀ n. ¬ np(n));(∃ n. np(max∞(np).n)) ∧ (∀ m. np(m) → ¬ max∞(np) < ⌜m⌝ ));
comment: definition justified by theorem maxinf-skolemf;
stutf-def : ⊦ stutf(nσ) ↔ nσ ≠ [] ∧ nσ[0] = 0 ∧ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n + 1] = nσ[n] ∨ nσ[n + 1] = nσ[n] + 1);
monle-def : ⊦ mon≤(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] ≤ nσ[n + 1]);
monls-def : ⊦ mon<(nσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # nσ → nσ[n] < nσ[n + 1]);
leninv-def : ⊦ leninv(nσ) = max∞(λ n. n ≠ 0 → (∃ m. ⌜m⌝ < # nσ ∧ nσ[m] = n - 1 ∧ ¬(# nσ = ∞ ∧ (∀ m0. m < m0 → nσ[m0] = n - 1))));
inv-def
: ⊦ stutf(nσ)
→ inv(nσ)
= (leninv(nσ) = ∞ ⊃ ⌜λ m. max∞(λ n. ⌜n⌝ < # nσ ∧ nσ[n] = m).n⌝ ;⌜λ m. max∞(λ n. ⌜n⌝ < # nσ ∧ nσ[n] = m).n⌝ to leninv(nσ).n);
min-def
: ⊦ mon<(nσ)
→ (nσ = []
⊃ min(nσ, n) = 0
;(# nσ ≠ ∞ ∧ nσ[(# nσ).n - 1] < n
⊃ min(nσ, n) = (# nσ).n
;⌜min(nσ, n)⌝ < # nσ ∧ n ≤ nσ[min(nσ, n)] ∧ (∀ m. ⌜m⌝ < # nσ ∧ n ≤ nσ[m] → min(nσ, n) ≤ m)
)
);
comment: Skolem function justified by theorems min-skolemf;
end enrich