---

Step * of Lemma expr_wf

∀[x:ℝ]. (expr(x) ∈ {y:ℝ| y = e^x} )
BY
{ ((Auto
    THEN (Assert TERMOF{converges-to-rexp-ext:o, 1:l} x ∈ lim n→∞.approx-rexp(x;n) = e^x BY
                Auto)
    THEN RW  (AddrC [2] (TagC (mk_tag_term 2))) (-1))
   THEN (InstLemma `req-from-converges` 
         [⌜λ2n.approx-rexp(x;n)⌝;⌜e^x⌝;⌜λk.(k
                                           + (k ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                     then 1
                                                     else 3^(((x 1) + 1) ÷ 2) + 1)
                                           + 1)⌝]⋅
         THENA Auto
         )
   THEN Reduce -1
   THEN (Assert ⌜cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                                    + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                                    then 1
                                                                    else 3^(((x 1) + 1) ÷ 2) + 1)
                                                    + 1)) ~ expr(x)⌝⋅
         THENA (RepUR ``expr approx-rexp`` 0
                THEN (GenConclTerm ⌜(((x 1) + 1) ÷ 2) + 1⌝⋅ THENA Auto)
                THEN CallByValueReduceOn ⌜v⌝ 0⋅
                THEN Auto)
         )) }

1
1. x : ℝ
2. λk.(k + (k ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)  then 1  else 3^(((x 1) + 1) ÷ 2) + 1) + 1)
   ∈ lim n→∞.approx-rexp(x;n) = e^x
3. e^x
= cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                     + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                     then 1
                                                     else 3^(((x 1) + 1) ÷ 2) + 1)
                                     + 1))
4. cauchy-limit(n.approx-rexp(x;n);λk.((2 * k)
                                      + ((2 * k) ÷ if ((((x 1) + 1) ÷ 2) + 1) < (0)
                                                      then 1
                                                      else 3^(((x 1) + 1) ÷ 2) + 1)
                                      + 1)) ~ expr(x)
⊢ expr(x) ∈ {y:ℝ| y = e^x} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (expr(x)  \mmember{}  \{y:\mBbbR{}|  y  =  e\^{}x\}  )


By

---

Latex:
((Auto
    THEN  (Assert  TERMOF\{converges-to-rexp-ext:o,  1:l\}  x  \mmember{}  lim  n\mrightarrow{}\minfty{}.approx-rexp(x;n)  =  e\^{}x  BY
                            Auto)
    THEN  RW    (AddrC  [2]  (TagC  (mk\_tag\_term  2)))  (-1))
  THEN  (InstLemma  `req-from-converges` 
              [\mkleeneopen{}\mlambda{}\msubtwo{}n.approx-rexp(x;n)\mkleeneclose{};\mkleeneopen{}e\^{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}k.(k
                                                                                  +  (k  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)
                                                                                                      then  1
                                                                                                      else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)
                                                                                  +  1)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  -1
  THEN  (Assert  \mkleeneopen{}cauchy-limit(n.approx-rexp(x;n);\mlambda{}k.((2  *  k)
                                                                                                    +  ((2  *  k)  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)
                                                                                                                                    then  1
                                                                                                                                    else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)
                                                                                                    +  1))  \msim{}  expr(x)\mkleeneclose{}\mcdot{}
              THENA  (RepUR  ``expr  approx-rexp``  0
                            THEN  (GenConclTerm  \mkleeneopen{}(((x  1)  +  1)  \mdiv{}  2)  +  1\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{}
                            THEN  Auto)
              ))

---

Home Index