---

Step * 1 2 1 of Lemma inhabited-covers-real-implies


1. [A] : ℝ ⟶ ℙ
2. [B] : ℝ ⟶ ℙ
3. a : ℝ
4. A[a]
5. b : ℝ
6. B[b]
7. d : r:ℝ ⟶ (A[r] + B[r])
8. h : ℕ ⟶ (ℝ × ℝ)
9. ∀n:ℕ
     (A[fst(h[n])]
     ∧ B[snd(h[n])]
     ∧ ((h[n + 1] = let a,b = h[n] in <a, (a + b/r(2))> ∈ (ℝ × ℝ))
       ∨ (h[n + 1] = let a,b = h[n] in <(a + b/r(2)), b> ∈ (ℝ × ℝ))))
10. n : ℕ
⊢ (((fst(h[n + 1])) = (fst(h[n]))) ∧ ((snd(h[n + 1])) = ((fst(h[n])) + (snd(h[n]))/r(2))))
∨ (((fst(h[n + 1])) = ((fst(h[n])) + (snd(h[n]))/r(2))) ∧ ((snd(h[n + 1])) = (snd(h[n]))))
BY
{ ((InstHyp [⌜n⌝] (-2)⋅ THENA Auto)
   THEN ExRepD
   THEN ParallelLast
   THEN (MoveToConcl (-1) THEN (GenConclTerm ⌜h[n]⌝⋅ THENA Auto))
   THEN ((D -2 THEN Reduce 0) THEN Auto)
   THEN RWO "16" 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
2.  [B]  :  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}
3.  a  :  \mBbbR{}
4.  A[a]
5.  b  :  \mBbbR{}
6.  B[b]
7.  d  :  r:\mBbbR{}  {}\mrightarrow{}  (A[r]  +  B[r])
8.  h  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbR{}  \mtimes{}  \mBbbR{})
9.  \mforall{}n:\mBbbN{}
          (A[fst(h[n])]
          \mwedge{}  B[snd(h[n])]
          \mwedge{}  ((h[n  +  1]  =  let  a,b  =  h[n]  in  <a,  (a  +  b/r(2))>)
              \mvee{}  (h[n  +  1]  =  let  a,b  =  h[n]  in  <(a  +  b/r(2)),  b>)))
10.  n  :  \mBbbN{}
\mvdash{}  (((fst(h[n  +  1]))  =  (fst(h[n])))  \mwedge{}  ((snd(h[n  +  1]))  =  ((fst(h[n]))  +  (snd(h[n]))/r(2))))
\mvee{}  (((fst(h[n  +  1]))  =  ((fst(h[n]))  +  (snd(h[n]))/r(2)))  \mwedge{}  ((snd(h[n  +  1]))  =  (snd(h[n]))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  ParallelLast
  THEN  (MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}h[n]\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  ((D  -2  THEN  Reduce  0)  THEN  Auto)
  THEN  RWO  "16"  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index