---

Step * 1 1 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))
⊢ ¬(∀k:{i..j-}. (F k))
BY
{ (D -1 THEN D 0 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.  \mexists{}k:\{i..j\msupminus{}\}.  (\mneg{}(F  k))
\mvdash{}  \mneg{}(\mforall{}k:\{i..j\msupminus{}\}.  (F  k))


By

---

Latex:
(D  -1  THEN  D  0  THEN  Auto)

---

Home Index