Step * 2 2 1 of Lemma decidable__exists_length


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]
BY
(ExRepD THEN With ⌜L⌝ (D 0)⋅ THEN Auto) }

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. 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