---

Step * of Lemma decidable__exists_length

∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
  ((∀L:T List. Dec(P[L])) ⇒ (∃k:ℕ. T ~ ℕk) ⇒ (∀n:ℕ. Dec(∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L]))))
BY
{ (Auto THEN ExRepD THEN Assert ⌜{as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n⌝⋅) }

1
.....assertion..... 
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
⊢ {as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n

2
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
7. {as:T List| ||as|| = n ∈ ℤ}  ~ ℕk^n
⊢ Dec(∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L]))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}L:T  List.  Dec(P[L]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  Dec(\mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  P[L]))))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  Assert  \mkleeneopen{}\{as:T  List|  ||as||  =  n\}    \msim{}  \mBbbN{}k\^{}n\mkleeneclose{}\mcdot{})

---

Home Index