---

Step * of Lemma approx-rexp_wf

∀[x:ℝ]. ∀[n:ℕ].  (approx-rexp(x;n) ∈ ℝ)
BY
{ (Auto
   THEN Unfold `approx-rexp` 0
   THEN (GenConclTerm ⌜(((x 1) + 1) ÷ 2) + 1⌝⋅ THENA Auto)
   THEN CaseNat 0 `n'
   THEN Reduce 0
   THEN ((CallByValueReduce 0 ORELSE Auto) THENA Auto)
   THEN (Decide ⌜v < 0⌝⋅ THENA Auto)
   THEN (Reduce 0 THENA Auto)) }

1
1. x : ℝ
2. n : ℕ
3. v : ℤ
4. ((((x 1) + 1) ÷ 2) + 1) = v ∈ ℤ
5. ¬(n = 0 ∈ ℤ)
6. v < 0
⊢ eval nc = n * 1 in
  eval m = 2 * nc in
  eval a = (x m) - 2 in
    (e^(r(a))/2 * m within 1/nc) ∈ ℝ

2
1. x : ℝ
2. n : ℕ
3. v : ℤ
4. ((((x 1) + 1) ÷ 2) + 1) = v ∈ ℤ
5. ¬(n = 0 ∈ ℤ)
6. ¬v < 0
⊢ eval c = 3^v in
  eval nc = n * c in
  eval m = 2 * nc in
  eval a = (x m) - 2 in
    (e^(r(a))/2 * m within 1/nc) ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[n:\mBbbN{}].    (approx-rexp(x;n)  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto
  THEN  Unfold  `approx-rexp`  0
  THEN  (GenConclTerm  \mkleeneopen{}(((x  1)  +  1)  \mdiv{}  2)  +  1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  CaseNat  0  `n'
  THEN  Reduce  0
  THEN  ((CallByValueReduce  0  ORELSE  Auto)  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}v  <  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Reduce  0  THENA  Auto))

---

Home Index