---

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


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
BY
{ (((D -1 With ⌜r0⌝  THENA Auto) THEN (D -1 With ⌜r1⌝  THENA Auto) THEN Reduce -1)
   THEN (Subst' fix((λf,n. if 4 <z |r1 (n + 1)| then 1 else f (n + 1) fi )) 0 ~ 1 -1 THENA ByComputation 0)
   ) }

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(ℤ)
⊢ False

---

Latex:

---

Latex:

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.  \mforall{}x,y:\mBbbR{}.
          (((\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))
\mvdash{}  False


By

---

Latex:
(((D  -1  With  \mkleeneopen{}r0\mkleeneclose{}    THENA  Auto)  THEN  (D  -1  With  \mkleeneopen{}r1\mkleeneclose{}    THENA  Auto)  THEN  Reduce  -1)
  THEN  (Subst'  fix((\mlambda{}f,n.  if  4  <z  |r1  (n  +  1)|  then  1  else  f  (n  +  1)  fi  ))  0  \msim{}  1  -1
              THENA  ByComputation  0
              )
  )

---

Home Index