---

Step * 1 1 1 1 1 of Lemma no-weak-limited-omniscience


1. n : ℕ
2. ∀g:ℕ ⟶ 𝔹. ((∀i:ℕn. ff = g i) ⇒ (∀n:ℕ. ff = ff ⇐⇒ ∀n:ℕ. g n = ff))
3. (∀n:ℕ. ff = ff) ⇐ ∀n@0:ℕ. (λi.n <z i) n@0 = ff
4. ∀n@0:ℕ. n <z n@0 = ff
5. n <z n + 1 = ff
⊢ False
BY
{ ((RWO "eqff_to_assert" (-1) THENA Auto) THEN RW assert_pushdownC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((\mforall{}i:\mBbbN{}n.  ff  =  g  i)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  ff  =  ff  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}.  g  n  =  ff))
3.  (\mforall{}n:\mBbbN{}.  ff  =  ff)  \mLeftarrow{}{}  \mforall{}n@0:\mBbbN{}.  (\mlambda{}i.n  <z  i)  n@0  =  ff
4.  \mforall{}n@0:\mBbbN{}.  n  <z  n@0  =  ff
5.  n  <z  n  +  1  =  ff
\mvdash{}  False


By

---

Latex:
((RWO  "eqff\_to\_assert"  (-1)  THENA  Auto)  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index