|
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.19 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.
|
