Step * 2 2 of Lemma decidable__exists_length


1. [T] Type
2. [P] (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. : ℕ
5. ~ ℕk
6. : ℕ
7. {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. 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]))
BY
ParallelLast⋅ }

1
1. Type
2. (T List) ⟶ ℙ
3. ∀L:T List. Dec(P[L])
4. : ℕ
5. ~ ℕk
6. : ℕ
7. {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. 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]


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.  \mneg{}(\mexists{}x:\mBbbN{}k\^{}n.  P[g  x])
\mvdash{}  \mneg{}(\mexists{}L:T  List.  ((||L||  =  n)  \mwedge{}  P[L]))


By


Latex:
ParallelLast\mcdot{}




Home Index