|
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]
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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
