---

Step * 2 1 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. x : ℕk^n
13. P[g x]
⊢ ||g x|| = n ∈ ℤ
BY
{ (GenConclAtAddr [2;1] THEN D (-2)⋅ THEN Auto) }

---

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.  x  :  \mBbbN{}k\^{}n
13.  P[g  x]
\mvdash{}  ||g  x||  =  n


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  D  (-2)\mcdot{}  THEN  Auto)

---

Home Index