---

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

.....antecedent..... 
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
⊢ ∀x,y:ℝ.
    ((x = y)
    ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)
       = ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) y)
       ∈ partial(ℤ)))
BY
{ ((InstHyp [⌜0⌝] (-1)⋅ THENA Auto)
   THEN Auto
   THEN (RWO "equal-partial" 0 THENA Auto)
   THEN Assert ⌜(∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|))
                ∧ (∀x:ℝ
                     (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
                     ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x) = 1 ∈ ℤ)))⌝⋅) }

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. y : ℝ
5. x = y
⊢ (∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|))
∧ (∀x:ℝ
     (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
     ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x) = 1 ∈ ℤ)))

2
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
6. (∀x:ℝ. (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓ ⇐⇒ r0 < |x|))
∧ (∀x:ℝ
     (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
     ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x) = 1 ∈ ℤ)))
⊢ uiff(((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓;((λx.(fix((λf,n. if 4 <z |x (n + 1)|
                                                                                            then 1
                                                                                            else f (n + 1)
                                                                                            fi )) 
                                                                                  0)) 
                                                                             y)↓)
∧ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)↓
  ⇒ (((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x)
     = ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) y)
     ∈ ℤ))

---

Latex:

---

Latex:
.....antecedent..... 
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{}))
\mvdash{}  \mforall{}x,y:\mBbbR{}.
        ((x  =  y)
        {}\mRightarrow{}  (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)
              =  ((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  y)))


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Auto
  THEN  (RWO  "equal-partial"  0  THENA  Auto)
  THEN  Assert  \mkleeneopen{}(\mforall{}x:\mBbbR{}
                                  (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)\mdownarrow{}
                                  \mLeftarrow{}{}\mRightarrow{}  r0  <  |x|))
                            \mwedge{}  (\mforall{}x:\mBbbR{}
                                      (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)\mdownarrow{}
                                      {}\mRightarrow{}  (((\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0))  x)  =  1))\000C)\mkleeneclose{}\mcdot{})

---

Home Index