---

Step * 1 1 1 of Lemma expr_wf


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 = expr(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)) ∈ ℝ
BY
{ ((InstLemma `converges-cauchy-witness` 
    [⌜λ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 GenConclAtAddr [2;2]
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mlambda{}k.(k  +  (k  \mdiv{}  if  ((((x  1)  +  1)  \mdiv{}  2)  +  1)  <  (0)    then  1    else  3\^{}(((x  1)  +  1)  \mdiv{}  2)  +  1)  +  1)
      \mmember{}  lim  n\mrightarrow{}\minfty{}.approx-rexp(x;n)  =  e\^{}x
3.  e\^{}x  =  expr(x)
\mvdash{}  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))  \mmember{}  \mBbbR{}


By

---

Latex:
((InstLemma  `converges-cauchy-witness` 
    [\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  GenConclAtAddr  [2;2]
  THEN  Auto)

---

Home Index