| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle nn_log.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Generalized log function (without ln/exp) % % Author: David Lester, Manchester University & NIA % % Version 1.0 19/08/08 Initial version (DRL) % %------------------------------------------------------------------------------ nn_log: THEORY BEGIN IMPORTING rational_props_aux, nn_root, nn_rational_expt, nnreal_expt a,b,x,y,z: VAR nnreal q: VAR nnrat px,py,pa,pb, delta,r, epsilon: VAR posreal ne1x: VAR {r | r /= 1} gt1x,gt1y: VAR {r | r > 1} lt1x,lt1y: VAR {r | r < 1} log_gt1(gt1x):[{r | r>=1}->nnreal] = inverse[nnreal,{r | r>=1}](lambda x: nnreal_expt(gt1x,x)) log_lt1(lt1x):[{r | r<=1}->nnreal] = inverse[nnreal,{r | r<=1}](lambda x: nnreal_expt(lt1x,x)) nn_log(ne1x)(y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}):nnreal = IF ne1x>1 THEN log_gt1(ne1x)(y) ELSE log_lt1(ne1x)(y) ENDIF nn_log_expt: LEMMA nn_log(ne1x)(nnreal_expt(ne1x,y)) = y nn_expt_log: LEMMA FORALL (y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}): nnreal_expt(ne1x,nn_log(ne1x)(y)) = y nn_log_plus: LEMMA FORALL (x,y:{r | ne1x>1 AND r>=1 OR ne1x<1 AND r<=1}): nn_log(ne1x)(x*y) = nn_log(ne1x)(x) + nn_log(ne1x)(y) nn_log_1: LEMMA nn_log(ne1x)(1) = 0 nn_log_ne1x: LEMMA nn_log(ne1x)(ne1x) = 1 nn_log_gt1: LEMMA nn_log(gt1x)(gt1y) > 1 IFF gt1y > gt1x nn_inv_base_log: LEMMA FORALL (y:{r | ne1x>1 AND r<=1 OR ne1x<1 AND r>=1}): nn_log(1/ne1x)(y) = nn_log(ne1x)(1/y) nn_log_increasing: LEMMA 1 < x AND x < y => nn_log(gt1x)(x) < nn_log(gt1x)(y) END nn_log ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28