---

Step * 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. Dec(∃k:{i..j-}. (¬(F k)))
⊢ Dec(∀k:{i..j-}. (F k))
BY
{ ((D -1 THENL [OrRight; OrLeft]) THEN Auto) }

1
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))

2
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

---

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.  Dec(\mexists{}k:\{i..j\msupminus{}\}.  (\mneg{}(F  k)))
\mvdash{}  Dec(\mforall{}k:\{i..j\msupminus{}\}.  (F  k))


By

---

Latex:
((D  -1  THENL  [OrRight;  OrLeft])  THEN  Auto)

---

Home Index