| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle nn_rational_expt.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Power function for nnx^nnq % % Author: David Lester, Manchester University & NIA % % Version 1.0 19/08/08 Initial version (DRL) %------------------------------------------------------------------------------ nn_rational_expt: THEORY BEGIN IMPORTING rational_props_aux, nn_root x,y,z,x1,x2: VAR nnreal px,py,epsilon,delta: VAR posreal q,r: VAR nnrat pq: VAR posrat n: VAR nat pn: VAR posnat nn_rational_expt(x,q):nnreal = nn_root(expt(x,numerator(q)),denominator(q)) nn_rational_expt_nat_rew: LEMMA nn_rational_expt(x,n) = x^n nn_rational_expt_root_rew: LEMMA nn_rational_expt(x,1/pn) = nn_root(x,pn) nn_rational_expt_rat_rew: LEMMA nn_rational_expt(x,n/pn) = nn_root(x^n,pn) nn_rational_expt_strict_increasing: LEMMA x < y => nn_rational_expt(x,pq) < nn_rational_expt(y,pq) nn_rational_expt_0q: LEMMA nn_rational_expt(0,q) = IF q = 0 THEN 1 ELSE 0 ENDIF nn_rational_expt_1q: LEMMA nn_rational_expt(1,q) = 1 nn_rational_expt_x1: LEMMA nn_rational_expt(x,1) = x nn_rational_expt_is_0: LEMMA nn_rational_expt(x,q) = 0 IFF x = 0 AND q /= 0 nn_rational_expt_pos: LEMMA nn_rational_expt(px,q) > 0 nn_rational_expt_gt1: LEMMA nn_rational_expt(x,pq) > 1 IFF x > 1 nn_rational_expt_lt1: LEMMA nn_rational_expt(x,pq) < 1 IFF x < 1 mult_nn_rational_expt: LEMMA nn_rational_expt(x*y,q) = nn_rational_expt(x,q)*nn_rational_expt(y,q) inv_nn_rational_expt: LEMMA nn_rational_expt(1/px,q) = 1/nn_rational_expt(px,q) div_nn_rational_expt: LEMMA nn_rational_expt(x/py,q) = nn_rational_expt(x,q)/nn_rational_expt(py,q) nn_rational_expt_plus: LEMMA nn_rational_expt(x,q+r) = nn_rational_expt(x,q)*nn_rational_expt(x,r) nn_rational_expt_times:LEMMA nn_rational_expt(x,q*r) = nn_rational_expt(nn_rational_expt(x,q),r) nn_rational_expt_decreasing: LEMMA q < r AND 0 < x AND x < 1 => nn_rational_expt(x,q) > nn_rational_expt(x,r) nn_rational_expt_increasing: LEMMA q < r AND 1 < x => nn_rational_expt(x,q) < nn_rational_expt(x,r) nn_rational_expt_def: LEMMA nn_rational_expt(x,q) = expt(nn_root(x,denominator(q)),numerator(q)) continuous_alt_nn_rational_expt: LEMMA EXISTS delta: FORALL x2: abs(x1-x2) < delta => abs(nn_rational_expt(x1,q)-nn_rational_expt(x2,q)) < epsilon nn_rational_expt_approx_gt1: LEMMA x > 1 AND y > 1 => EXISTS q: abs(nn_rational_expt(x,q)-y) < epsilon END nn_rational_expt ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28