| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle expt_rew.pvs Sprache: PVS |
|||||||||
|
expt_rew: THEORY
%------------------------------------------------------------------------------ % % EXPERIMENTAL theory -- not ready for prime time % %------------------------------------------------------------------------------ BEGIN pn: VAR posnat AUTO_REWRITE+ expt_x0_aux % LEMMA expt(x, 0) = 1 AUTO_REWRITE+ expt_x1_aux % LEMMA expt(x, 1) = x AUTO_REWRITE+ expt_1n_aux % LEMMA expt(1, n) = 1 AUTO_REWRITE+ expt_of_mult % LEMMA expt(x*y, n) = expt(x, n) * expt(y, n) AUTO_REWRITE+ expt_of_div % LEMMA expt(x/z, n) = expt(x, n) / expt(z, n) AUTO_REWRITE+ expt_of_inv % LEMMA expt(1 / z, n) = 1 / expt(z, n) AUTO_REWRITE+ expt_x0 % LEMMA x^0 = 1 AUTO_REWRITE+ expt_x1 % LEMMA x^1 = x AUTO_REWRITE+ expt_1i % LEMMA 1^i = 1 i: VAR int n0x, n0y: VAR nzreal zero_hat : LEMMA 0^pn = 0 mult_hat : LEMMA n0x^i * n0y^i = (n0x * n0y) ^i div_hat : LEMMA n0x^i / n0y^i = (n0x / n0y)^i inv_hat : LEMMA 1 / n0x^i = (1 / n0x)^i AUTO_REWRITE+ zero_hat AUTO_REWRITE+ mult_hat AUTO_REWRITE+ div_hat AUTO_REWRITE+ inv_hat AUTO_REWRITE+ pos_expt_gt % LEMMA n < b^n AUTO_REWRITE+ expt_ge1 % LEMMA b^n >= 1 AUTO_REWRITE+ expt_gt1_pos % LEMMA gt1x^pm >= gt1x AUTO_REWRITE+ expt_gt1_neg % LEMMA gt1x^(-pm) < 1 AUTO_REWRITE+ expt_gt1_nonpos % LEMMA gt1x^(-m) <= 1 AUTO_REWRITE+ expt_lt1_bound1 % LEMMA expt(lt1x, n) <= 1 AUTO_REWRITE+ expt_lt1_bound2 % LEMMA expt(lt1x, pn) < 1 AUTO_REWRITE+ expt_gt1_bound1 % LEMMA 1 <= expt(gt1x, n) AUTO_REWRITE+ expt_gt1_bound2 % LEMMA 1 < expt(gt1x, pn) END expt_rew ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28