Step
*
2
1
2
2
1
of Lemma
simple_fan_theorem'
1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ
2. ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
3. ∀n:ℕ. ∀s:ℕn ⟶ 𝔹. Dec(X[n;s])
4. n : ℕ@i
5. s : ℕn ⟶ 𝔹@i
6. ∀t:𝔹. (∃k:ℕ [(∀f:ℕ ⟶ 𝔹. ∃m:ℕk. X[(n + 1) + m;seq-append(n + 1;m;s++t;f)])])
7. k : ℕ
8. ∀f:ℕ ⟶ 𝔹. ∃m:ℕk. X[(n + 1) + m;seq-append(n + 1;m;s++tt;f)]
9. k1 : ℕ
10. ∀f:ℕ ⟶ 𝔹. ∃m:ℕk1. X[(n + 1) + m;seq-append(n + 1;m;s++ff;f)]
11. f : ℕ ⟶ 𝔹
12. ¬↑(f 0)
13. m : ℕk
14. X[(n + 1) + m;seq-append(n + 1;m;s++tt;λn.(f (n + 1)))]
15. m1 : ℤ
16. 0 ≤ m1
17. m1 < k1
18. X[(n + 1) + m1;seq-append(n + 1;m1;s++ff;λn.(f (n + 1)))]
19. f 0 = ff
⊢ m1 < (imax(k;k1) + 1) - 1
BY
{ (RWO "imax_unfold" 0 THEN Auto) }
Latex:
Latex:
1. X : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} \mBbbB{}) {}\mrightarrow{} \mBbbP{}
2. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. (\mdownarrow{}\mexists{}n:\mBbbN{}. X[n;f])
3. \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} \mBbbB{}. Dec(X[n;s])
4. n : \mBbbN{}@i
5. s : \mBbbN{}n {}\mrightarrow{} \mBbbB{}@i
6. \mforall{}t:\mBbbB{}. (\mexists{}k:\mBbbN{} [(\mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}m:\mBbbN{}k. X[(n + 1) + m;seq-append(n + 1;m;s++t;f)])])
7. k : \mBbbN{}
8. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}m:\mBbbN{}k. X[(n + 1) + m;seq-append(n + 1;m;s++tt;f)]
9. k1 : \mBbbN{}
10. \mforall{}f:\mBbbN{} {}\mrightarrow{} \mBbbB{}. \mexists{}m:\mBbbN{}k1. X[(n + 1) + m;seq-append(n + 1;m;s++ff;f)]
11. f : \mBbbN{} {}\mrightarrow{} \mBbbB{}
12. \mneg{}\muparrow{}(f 0)
13. m : \mBbbN{}k
14. X[(n + 1) + m;seq-append(n + 1;m;s++tt;\mlambda{}n.(f (n + 1)))]
15. m1 : \mBbbZ{}
16. 0 \mleq{} m1
17. m1 < k1
18. X[(n + 1) + m1;seq-append(n + 1;m1;s++ff;\mlambda{}n.(f (n + 1)))]
19. f 0 = ff
\mvdash{} m1 < (imax(k;k1) + 1) - 1
By
Latex:
(RWO "imax\_unfold" 0 THEN Auto)
Home
Index