Suchen Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Haftungshinweis

Bemerkung: zur Agenda Produktseite wechseln Projekt Beratung

Suchen Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quellcode-Bibliothek ln_exp_def.pvs Sprache: PVS

%
% David Lester, Manchester University
% 10/10/08
%
% Linking log and ^ to exp and ln.

ln_exp_def: THEORY

BEGIN

  IMPORTING log,
            real_expt,
            lnexp_fnd@ln_exp

  i:    VAR int
  n:    VAR nat
  q:    VAR nnrat
  pn:   VAR posnat
  x:    VAR real
  z:    VAR nnreal
  a,r,y: VAR posreal
  ne1x: VAR {r | r /= 1}

  expt_exp:    LEMMA expt(y,n) = exp(n*ln(y))

  nn_root_def: LEMMA nn_root(z,pn) = IF z = 0 THEN 0 ELSE exp(ln(z)/pn) ENDIF

  nn_rational_expt_def: LEMMA nn_rational_expt(y,q) = exp(q*ln(y))

  nnreal_expt_def:      LEMMA nnreal_expt(y,z) = exp(z*ln(y))

  real_expt_def:        LEMMA y^x = exp(x*ln(y))

  nn_log_def: LEMMA r > 1 AND y >= 1 OR r < 1 AND y <= 1 =>
                    nn_log(r)(y) = ln(y)/ln(r)

  log_def:    LEMMA log(ne1x,y) = ln(y)/ln(ne1x)

  IMPORTING analysis@continuous_functions,
            analysis@derivatives

  log_continuous: LEMMA continuous?[posreal](log(ne1x))
  log_derivable:  LEMMA derivable?[posreal](log(ne1x)) AND
                        deriv[posreal](log(ne1x)) = (LAMBDA y: 1/(ln(ne1x)*y))

  real_expt_continuous: LEMMA continuous?[posreal](lambda y: y^x)
  real_expt_derivable:  LEMMA derivable?[posreal](lambda y: y^x) AND
                              deriv[posreal](lambda y: y^x)
                                   = (lambda y: x*y^(x-1))

END ln_exp_def

quality95%

¤ 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.13Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.