---

Step * of Lemma decidable-all-finite

∀[T:Type]. (finite(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∀t:T. P[t]))))
BY
{ (InstLemma `decidable-exists-finite` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN Auto
   THEN (Assert Dec(∃t:T. (¬P[t])) BY
               Auto)
   THEN (D -1 THENL [((OrRight THENM D 0) THEN Auto); ((OrLeft THEN Auto) THEN (SupposeNot THEN D -3) THEN Auto)])) }

1
1. T : Type
2. finite(T)
3. ∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))
4. P : T ⟶ ℙ
5. ∀t:T. Dec(P[t])
6. ∃t:T. (¬P[t])
7. ∀t:T. P[t]
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite(T)  {}\mRightarrow{}  (\mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:T.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mforall{}t:T.  P[t]))))


By

---

Latex:
(InstLemma  `decidable-exists-finite`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  (Assert  Dec(\mexists{}t:T.  (\mneg{}P[t]))  BY
                          Auto)
  THEN  (D  -1
              THENL  [((OrRight  THENM  D  0)  THEN  Auto)
                          ;  ((OrLeft  THEN  Auto)  THEN  (SupposeNot  THEN  D  -3)  THEN  Auto)]
  ))

---

Home Index