---

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

.....wf..... 
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:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
7. x1 : ℝ
8. (fix((λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi )) 0)↓
9. λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi  ∈ (ℕ ⟶ partial(ℤ)) ⟶ ℕ ⟶ partial(ℤ)
10. ∀j,k:ℕ.  (λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi ^j ⊥ k ∈ partial(ℤ))
11. k : ℕ
⊢ istype((fix((λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi )) k)↓)
BY
{ ((InstLemma `has-value_wf-partial` [⌜ℤ⌝]⋅ THENA Auto) THEN At ⌜ℙ⌝ (D 0)⋅ THEN BHyp -1) }

1
.....wf..... 
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:ℝ. ((r0 < |x|) ⇒ ((λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)) x ~ 1))
7. x1 : ℝ
8. (fix((λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi )) 0)↓
9. λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi  ∈ (ℕ ⟶ partial(ℤ)) ⟶ ℕ ⟶ partial(ℤ)
10. ∀j,k:ℕ.  (λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi ^j ⊥ k ∈ partial(ℤ))
11. k : ℕ
12. ∀[a:partial(ℤ)]. ((a)↓ ∈ ℙ)
⊢ fix((λf,n. if 4 <z |x1 (n + 1)| then 1 else f (n + 1) fi )) k ∈ partial(ℤ)

---

Latex:

---

Latex:
.....wf..... 
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
6.  \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))
7.  x1  :  \mBbbR{}
8.  (fix((\mlambda{}f,n.  if  4  <z  |x1  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)\mdownarrow{}
9.  \mlambda{}f,n.  if  4  <z  |x1  (n  +  1)|  then  1  else  f  (n  +  1)  fi    \mmember{}  (\mBbbN{}  {}\mrightarrow{}  partial(\mBbbZ{}))  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  partial(\mBbbZ{})
10.  \mforall{}j,k:\mBbbN{}.    (\mlambda{}f,n.  if  4  <z  |x1  (n  +  1)|  then  1  else  f  (n  +  1)  fi  \^{}j  \mbot{}  k  \mmember{}  partial(\mBbbZ{}))
11.  k  :  \mBbbN{}
\mvdash{}  istype((fix((\mlambda{}f,n.  if  4  <z  |x1  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  k)\mdownarrow{})


By

---

Latex:
((InstLemma  `has-value\_wf-partial`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  At  \mkleeneopen{}\mBbbP{}\mkleeneclose{}  (D  0)\mcdot{}  THEN  BHyp  -1)

---

Home Index