---

Step * 2 of Lemma dd_wf


1. d : ℕ+
2. x : ℝ
3. N : ℕ+
4. 10^d = N ∈ ℕ+
5. a : {a:Atom| a = "display-as" ∈ Atom} 
× {a:Atom| a = "decimal-rational" ∈ Atom} 
× {z:ℝ| z = x} 
× {n:ℕ+| n = d ∈ ℤ} 
× {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} 
6. <"display-as", "decimal-rational", x, d, eval N = N in eval N2 = N ÷ 2 in   x N2>
= a
∈ ({a:Atom| a = "display-as" ∈ Atom} 
  × {a:Atom| a = "decimal-rational" ∈ Atom} 
  × {z:ℝ| z = x} 
  × {n:ℕ+| n = d ∈ ℤ} 
  × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} )
⊢ let answer ⟵ a
  in answer ∈ {a:Atom| a = "display-as" ∈ Atom} 
  × {a:Atom| a = "decimal-rational" ∈ Atom} 
  × {z:ℝ| z = x} 
  × {n:ℕ+| n = d ∈ ℤ} 
  × {n:ℤ| |x - (r(n)/r(N))| ≤ (r(2)/r(N))} 
BY
{ (CallByValueReduce 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}\msupplus{}
2.  x  :  \mBbbR{}
3.  N  :  \mBbbN{}\msupplus{}
4.  10\^{}d  =  N
5.  a  :  \{a:Atom|  a  =  "display-as"\} 
\mtimes{}  \{a:Atom|  a  =  "decimal-rational"\} 
\mtimes{}  \{z:\mBbbR{}|  z  =  x\} 
\mtimes{}  \{n:\mBbbN{}\msupplus{}|  n  =  d\} 
\mtimes{}  \{n:\mBbbZ{}|  |x  -  (r(n)/r(N))|  \mleq{}  (r(2)/r(N))\} 
6.  <"display-as",  "decimal-rational",  x,  d,  eval  N  =  N  in  eval  N2  =  N  \mdiv{}  2  in      x  N2>  =  a
\mvdash{}  let  answer  \mleftarrow{}{}  a
    in  answer  \mmember{}  \{a:Atom|  a  =  "display-as"\} 
    \mtimes{}  \{a:Atom|  a  =  "decimal-rational"\} 
    \mtimes{}  \{z:\mBbbR{}|  z  =  x\} 
    \mtimes{}  \{n:\mBbbN{}\msupplus{}|  n  =  d\} 
    \mtimes{}  \{n:\mBbbZ{}|  |x  -  (r(n)/r(N))|  \mleq{}  (r(2)/r(N))\} 


By

---

Latex:
(CallByValueReduce  0\mcdot{}  THEN  Auto)

---

Home Index