ln_exp: THEORY BEGIN x,y,a: VAR real i: VAR integer e: real px,py: VAR posreal monotonic?(pp): bool = FORALL p1, p2: p1 <= p2 IMPLIES pp(p1) <= pp(p2) ln(px: posreal): real ln_mult: AXIOM ln(px*py) = ln(px) + ln(py) ln_div : AXIOM ln(px/py) = ln(px) - ln(py) ln_expt: AXIOM ln(px^i) = i*ln(px) ln_bij : AXIOM bijective?[posreal, real](ln) ln_1: LEMMA ln(1) = 0 exp(x): { py | x = ln(py)} exp_def : LEMMA exp = inverse(ln) ln_exp : LEMMA ln(exp(x)) = x exp_ln : LEMMA exp(ln(py)) = py e_def : AXIOM e = exp(1) exp_int : AXIOM exp(i) = e^i exp_sum : LEMMA exp(x+y) = exp(x)*exp(y) exp_diff: LEMMA exp(x-y) = exp(x)/exp(y) exp_scal: LEMMA exp(i*x) = exp(x)^i exp_0 : LEMMA exp(0) = 1 exp_1 : LEMMA exp(1) = e expt_alt_def: LEMMA x > 0 IMPLIES x^i = exp(i*ln(x)) exp_mono : LEMMA monotonic?(exp) large_exp: LEMMA (FORALL a: EXISTS x: a < exp(x)) small_exp: LEMMA (FORALL a: EXISTS x: exp(x) < a) END ln_exp