---

Step * 2 1 2 1 1 of Lemma filter_map_upto2

.....truecase..... 
1. t' : ℤ
2. [%1] : 0 < t'
3. ∀m:ℕ
     ∀[T:Type]
       ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
         ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) 
         supposing (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||
4. m : ℕ
5. [T] : Type
6. f : ℕ ⟶ T
7. P : T ⟶ 𝔹
8. 0 < t'
9. ↑(P (f (t' - 1)))
⊢ ((m + 1) ≤ ||filter(P;map(f;upto(t' - 1))) @ [f (t' - 1)]||)
⇒ (∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)))
BY
{ (((RWO "length_append" 0 THENA Auto) THEN Reduce 0 THEN Auto THEN Decide (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||⋅)
   THENA Auto
   ) }

1
1. t' : ℤ
2. [%1] : 0 < t'
3. ∀m:ℕ
     ∀[T:Type]
       ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
         ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) 
         supposing (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||
4. m : ℕ
5. [T] : Type
6. f : ℕ ⟶ T
7. P : T ⟶ 𝔹
8. 0 < t'
9. ↑(P (f (t' - 1)))
10. (m + 1) ≤ (||filter(P;map(f;upto(t' - 1)))|| + 1)
11. (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||
⊢ ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ))

2
1. t' : ℤ
2. [%1] : 0 < t'
3. ∀m:ℕ
     ∀[T:Type]
       ∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
         ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) 
         supposing (m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||
4. m : ℕ
5. [T] : Type
6. f : ℕ ⟶ T
7. P : T ⟶ 𝔹
8. 0 < t'
9. ↑(P (f (t' - 1)))
10. (m + 1) ≤ (||filter(P;map(f;upto(t' - 1)))|| + 1)
11. ¬((m + 1) ≤ ||filter(P;map(f;upto(t' - 1)))||)
⊢ ∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ))

---

Latex:

---

Latex:
.....truecase..... 
1.  t'  :  \mBbbZ{}
2.  [\%1]  :  0  <  t'
3.  \mforall{}m:\mBbbN{}
          \mforall{}[T:Type]
              \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.
                  \mexists{}t:\mBbbN{}.  ((\muparrow{}(P  (f  t)))  \mwedge{}  (||filter(P;map(f;upto(t)))||  =  m)) 
                  supposing  (m  +  1)  \mleq{}  ||filter(P;map(f;upto(t'  -  1)))||
4.  m  :  \mBbbN{}
5.  [T]  :  Type
6.  f  :  \mBbbN{}  {}\mrightarrow{}  T
7.  P  :  T  {}\mrightarrow{}  \mBbbB{}
8.  0  <  t'
9.  \muparrow{}(P  (f  (t'  -  1)))
\mvdash{}  ((m  +  1)  \mleq{}  ||filter(P;map(f;upto(t'  -  1)))  @  [f  (t'  -  1)]||)
{}\mRightarrow{}  (\mexists{}t:\mBbbN{}.  ((\muparrow{}(P  (f  t)))  \mwedge{}  (||filter(P;map(f;upto(t)))||  =  m)))


By

---

Latex:
(((RWO  "length\_append"  0  THENA  Auto)
    THEN  Reduce  0
    THEN  Auto
    THEN  Decide  (m  +  1)  \mleq{}  ||filter(P;map(f;upto(t'  -  1)))||\mcdot{})
  THENA  Auto
  )

---

Home Index