---

Step * 2 of Lemma decidable__exists_length


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]))
BY
{ (RepeatFor 2 (D -1)
   THEN Unfold `surject` -1
   THEN (Skolemize (-1) `g' THENA Auto)
   THEN (Assert ⌜Dec(∃x:ℕk^n. P[g x])⌝⋅ THEN Auto)
   THEN RepeatFor 2 (ParallelLast))⋅ }

1
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
7. f : {as:T List| ||as|| = n ∈ ℤ}  ⟶ ℕk^n
8. Inj({as:T List| ||as|| = n ∈ ℤ} ;ℕk^n;f)
9. ∀b:ℕk^n. ∃a:{as:T List| ||as|| = n ∈ ℤ} . ((f a) = b ∈ ℕk^n)
10. g : b:ℕk^n ⟶ {as:T List| ||as|| = n ∈ ℤ} 
11. ∀b:ℕk^n. ((f (g b)) = b ∈ ℕk^n)
12. ∃x:ℕk^n. P[g x]
⊢ ∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L])

2
1. [T] : Type
2. [P] : (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. k : ℕ
5. T ~ ℕk
6. n : ℕ
7. f : {as:T List| ||as|| = n ∈ ℤ}  ⟶ ℕk^n
8. Inj({as:T List| ||as|| = n ∈ ℤ} ;ℕk^n;f)
9. ∀b:ℕk^n. ∃a:{as:T List| ||as|| = n ∈ ℤ} . ((f a) = b ∈ ℕk^n)
10. g : b:ℕk^n ⟶ {as:T List| ||as|| = n ∈ ℤ} 
11. ∀b:ℕk^n. ((f (g b)) = b ∈ ℕk^n)
12. ¬(∃x:ℕk^n. P[g x])
⊢ ¬(∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L]))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}L:T  List.  Dec(P[L])
4.  k  :  \mBbbN{}
5.  T  \msim{}  \mBbbN{}k
6.  n  :  \mBbbN{}
7.  \{as:T  List|  ||as||  =  n\}    \msim{}  \mBbbN{}k\^{}n
\mvdash{}  Dec(\mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  P[L]))


By

---

Latex:
(RepeatFor  2  (D  -1)
  THEN  Unfold  `surject`  -1
  THEN  (Skolemize  (-1)  `g'  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}Dec(\mexists{}x:\mBbbN{}k\^{}n.  P[g  x])\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  RepeatFor  2  (ParallelLast))\mcdot{}

---

Home Index