| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quellcode-Bibliothek interval_lnexp.pvs Sprache: PVS |
|||||||||
|
%% interval_lnexp.pvs
interval_lnexp : THEORY BEGIN IMPORTING lnexp_fnd@exp_approx, lnexp_fnd@ln_approx, interval X,Y : VAR Interval x : VAR real n : VAR nat Exp(n)(X) : (Pos?) = [|exp_lb(lb(X),n),exp_ub(ub(X),n)|] Exp_fundamental: LEMMA X << Y IMPLIES Exp(n)(X) << Exp(n)(Y) Ln(n)(X) : Interval = if lb(X) > 0 AND ub(X) > 0 then [|ln_lb(lb(X),n),ln_ub(ub(X),n)|] else EmptyInterval endif % lemmas Ln_fundamental: LEMMA Pos?(Y) AND Proper?(X) AND X << Y IMPLIES Ln(n)(X) << Ln(n)(Y) Exp_inclusion : LEMMA x ## X IMPLIES exp(x) ## Exp(n)(X) % En En(n) : (Pos?) = Exp(n)([|1|]) Ln_inclusion : LEMMA Pos?(X) AND x ## X IMPLIES ln(x) ## Ln(n)(X) %% Safe version of ln and exp IMPORTING safe_arith safe_Ln(n) : [Interval->Interval] = Safe1(Ln(n)) safe_Exp(n) : [Interval->Interval] = Safe1(Exp(n)) %% Proper version of ln and exp IMPORTING proper_arith Xp : VAR ProperInterval XP : VAR PosInterval Proper_Ln : JUDGEMENT Ln(n)(XP) HAS_TYPE ProperInterval Proper_Exp : JUDGEMENT Exp(n)(Xp) HAS_TYPE ProperInterval proper_Ln(n)(XP) : ProperInterval = Ln(n)(XP) proper_Exp(n)(Xp) : PosInterval = Exp(n)(Xp) END interval_lnexp ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28