---

Step * 2 2 1 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. 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. ∃L:T List. ((||L|| = n ∈ ℤ) ∧ P[L])
⊢ ∃x:ℕk^n. P[g x]
BY
{ (ExRepD THEN With ⌜f L⌝ (D 0)⋅ THEN Auto) }

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. L : T List
13. ||L|| = n ∈ ℤ
14. P[L]
⊢ P[g (f 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.  f  :  \{as:T  List|  ||as||  =  n\}    {}\mrightarrow{}  \mBbbN{}k\^{}n
8.  Inj(\{as:T  List|  ||as||  =  n\}  ;\mBbbN{}k\^{}n;f)
9.  \mforall{}b:\mBbbN{}k\^{}n.  \mexists{}a:\{as:T  List|  ||as||  =  n\}  .  ((f  a)  =  b)
10.  g  :  b:\mBbbN{}k\^{}n  {}\mrightarrow{}  \{as:T  List|  ||as||  =  n\} 
11.  \mforall{}b:\mBbbN{}k\^{}n.  ((f  (g  b))  =  b)
12.  \mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  P[L])
\mvdash{}  \mexists{}x:\mBbbN{}k\^{}n.  P[g  x]


By

---

Latex:
(ExRepD  THEN  With  \mkleeneopen{}f  L\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index