% % David Lester, Manchester University % 10/10/08 % % Linking log and ^ to exp and ln. THEORY BEGIN IMPORTING log,VAR intVAR natVAR nnratVAR posnatVAR realVAR nnrealVAR posrealVAR {r | r /= 1}LEMMA expt(y,n) = exp(n*ln(y))LEMMA nn_root(z,pn) = IF z = 0 THEN 0 ELSE exp(ln(z)/pn) ENDIF LEMMA nn_rational_expt(y,q) = exp(q*ln(y))LEMMA nnreal_expt(y,z) = exp(z*ln(y))LEMMA y^x = exp(x*ln(y))LEMMA r > 1 AND y >= 1 OR r < 1 AND y <= 1 =>LEMMA log(ne1x,y) = ln(y)/ln(ne1x)IMPORTING analysis@continuous_functions,LEMMA continuous?[posreal](log(ne1x))LEMMA derivable?[posreal](log(ne1x)) AND LAMBDA y: 1/(ln(ne1x)*y))LEMMA continuous?[posreal](lambda y: y^x)LEMMA derivable?[posreal](lambda y: y^x) AND lambda y: y^x)lambda y: x*y^(x-1))END ln_exp_defquality 95%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
