---

Step * 1 2 of Lemma decidable__all_int_seg


1. i : ℤ@i
2. j : ℤ@i
3. [F] : {i..j-} ⟶ ℙ{u}
4. ∀k:{i..j-}. Dec(F k)@[u | i]
5. ¬(∃k:{i..j-}. (¬(F k)))
6. k : {i..j-}@i
⊢ F k
BY
{ (SupposeNot THEN D -3 THEN Auto) }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}@i
2.  j  :  \mBbbZ{}@i
3.  [F]  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}\{u\}
4.  \mforall{}k:\{i..j\msupminus{}\}.  Dec(F  k)@[u  |  i]
5.  \mneg{}(\mexists{}k:\{i..j\msupminus{}\}.  (\mneg{}(F  k)))
6.  k  :  \{i..j\msupminus{}\}@i
\mvdash{}  F  k


By

---

Latex:
(SupposeNot  THEN  D  -3  THEN  Auto)

---

Home Index