---

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

.....equality..... 
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. (fix((λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi )) 0) = 1 ∈ partial(ℤ)
⊢ fix((λf,n. if 4 <z |r0 (n + 1)| then 1 else f (n + 1) fi )) 0 ~ ⊥
BY
{ SqequalSqle⋅ }

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

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

---

Latex:

---

Latex:
.....equality..... 
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.  (fix((\mlambda{}f,n.  if  4  <z  |r0  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)  =  1
\mvdash{}  fix((\mlambda{}f,n.  if  4  <z  |r0  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0  \msim{}  \mbot{}


By

---

Latex:
SqequalSqle\mcdot{}

---

Home Index