---

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


1. discrete-type(partial(ℤ))
2. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
⊢ False
BY
{ ((D -2 With ⌜λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) 0)⌝  THENA Auto) THEN D -1) }

1
.....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(ℤ)))

2
1. ∀k:ℕ. (λx.(fix((λf,n. if 4 <z |x (n + 1)| then 1 else f (n + 1) fi )) k) ∈ ℝ ⟶ partial(ℤ))
2. ∀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(ℤ))
⊢ False

---

Latex:

---

Latex:

1.  discrete-type(partial(\mBbbZ{}))
2.  \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{}  False


By

---

Latex:
((D  -2  With  \mkleeneopen{}\mlambda{}x.(fix((\mlambda{}f,n.  if  4  <z  |x  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0)\mkleeneclose{}    THENA  Auto)  THEN  D  \000C-1)

---

Home Index