---

Step * 1 1 1 1 1 of Lemma partial-int-not-discrete

.....assertion..... 
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0) ∈ ℝ ⟶ partial(ℤ)
3. x : ℝ
4. y : ℝ
5. x = y
⊢ ∀x:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
BY
{ (RepeatFor 3 (Thin (-1))
   THEN Auto
   THEN D -1
   THEN Reduce 0
   THEN RepUR ``int-to-real`` -1
   THEN (Subst' (2 * n * 0) + 4 ~ 4 -1 THENA Auto)
   THEN (Assert ⌜∀k:ℕ. (k < n ⇒ ((fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) = 1 ∈ ℤ))⌝⋅
   THENM (BHyp -1 THEN Auto)
   )) }

1
.....assertion..... 
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0) ∈ ℝ ⟶ partial(ℤ)
3. x : ℝ
4. n : ℕ+
5. 4 < |x| n
⊢ ∀k:ℕ. (k < n ⇒ ((fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) = 1 ∈ ℤ))

---

Latex:

---

Latex:
.....assertion..... 
1.  \mforall{}k:\mBbbN{}.  (\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{}))
2.  \mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)  \mmember{}  \mBbbR{}  {}\mrightarrow{}  partial(\mBbbZ{})
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
5.  x  =  y
\mvdash{}  \mforall{}x:\mBbbR{}.  ((r0  <  |x|)  {}\mRightarrow{}  ((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x  \msim{}  1))


By

---

Latex:
(RepeatFor  3  (Thin  (-1))
  THEN  Auto
  THEN  D  -1
  THEN  Reduce  0
  THEN  RepUR  ``int-to-real``  -1
  THEN  (Subst'  (2  *  n  *  0)  +  4  \msim{}  4  -1  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mforall{}k:\mBbbN{}.  (k  <  n  {}\mRightarrow{}  ((fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)  =  1))\000C\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1  THEN  Auto)
  ))

---

Home Index