Quelle derivatives_lam.pvs Sprache: PVS

derivatives_lam[T: TYPE FROM real ]: THEORY
%------------------------------------------------------------------------------
% This theory has been created to support auto-rewriting, e.g.
%
%    auto-rewrite-theory "derivatives_lam[T]"
%
% or via special strategies
%------------------------------------------------------------------------------
BEGIN

  ASSUMING

    IMPORTING deriv_domain_def

    deriv_domain     : ASSUMPTION deriv_domain?[T]

    not_one_element  : ASSUMPTION not_one_element?[T]

  ENDASSUMING

  IMPORTING derivatives[T],
            reals@sq

  t   : VAR T
  a   : VAR real
  b   : VAR nzreal
  n   : VAR nat
  m   : VAR posnat
  f,g : VAR deriv_fun
  k   : VAR nz_deriv_fun

  derivable_id_lam     : LEMMA derivable?(LAMBDA(t):t)
  derivable_const_lam  : LEMMA derivable?(LAMBDA(t):a)
  derivable_add_lam    : LEMMA derivable?(LAMBDA(t):f(t)+g(t))
  derivable_mult_lam   : LEMMA derivable?(LAMBDA(t):f(t)*g(t))
  derivable_pow_lam    : LEMMA derivable?(LAMBDA(t):t^n)
  derivable_scal1_lam  : LEMMA derivable?(LAMBDA(t): a*f(t))
  derivable_scal2_lam  : LEMMA derivable?(LAMBDA(t): f(t)*a)
  derivable_neg_lam    : LEMMA derivable?(LAMBDA(t):-g(t))
  derivable_sub_lam    : LEMMA derivable?(LAMBDA(t):f(t)-g(t))
  derivable_sq_lam     : LEMMA derivable?(LAMBDA(t):sq(t))
  derivable_div_lam    : LEMMA derivable?(LAMBDA(t):f(t)/k(t))
  derivable_scald1_lam : LEMMA derivable?(LAMBDA(t): a/k(t))
  derivable_scald2_lam : LEMMA derivable?(LAMBDA(t): f(t)/b)

  deriv_id_lam         : LEMMA deriv(LAMBDA(t):t) = LAMBDA(t):1

  deriv_const_lam      : LEMMA deriv(LAMBDA(t):a) = LAMBDA(t):0

  deriv_add_lam        : LEMMA deriv(LAMBDA(t):f(t)+g(t)) = LAMBDA(t): deriv(f)(t) + deriv(g)(t)

  deriv_mult_lam       : LEMMA deriv(LAMBDA(t):f(t)*g(t))
                                 = LAMBDA(t):deriv(f)(t)*g(t) + deriv(g)(t)*f(t)

  deriv_pow_lam        : LEMMA deriv(LAMBDA(t):t^m) = LAMBDA(t):(m*t^(m-1))

  deriv_scal1_lam      : LEMMA deriv(LAMBDA(t): a*f(t)) = LAMBDA(t):a*deriv(f)(t)

  deriv_scal2_lam      : LEMMA deriv(LAMBDA(t): f(t)*a) = LAMBDA(t):a*deriv(f)(t)

  deriv_neg_lam        : LEMMA deriv(LAMBDA(t):-g(t)) = LAMBDA(t):-deriv(g)(t)

  deriv_sub_lam        : LEMMA deriv(LAMBDA(t):f(t)-g(t)) = LAMBDA(t):deriv(f)(t)-deriv(g)(t)

  deriv_sq_lam         : LEMMA deriv(LAMBDA(t):sq(t)) = LAMBDA(t):2*t

  deriv_div_lam        : LEMMA deriv(LAMBDA(t):f(t)/k(t))
                                  = LAMBDA(t):(deriv(f)(t)*k(t) - deriv(k)(t)*f(t)) / sq(k(t))

  deriv_scald1_lam     : LEMMA deriv(LAMBDA(t): a/k(t))
                                  = LAMBDA(t):-a*deriv(k)(t)/sq(k(t))

  deriv_scald2_lam     : LEMMA deriv(LAMBDA(t): f(t)/b) = LAMBDA(t):(deriv(f)(t))/b

END derivatives_lam

quality93%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.