---

Step * of Lemma filter_map_upto

∀[T:Type]. ∀[i,j:ℕ].
  ∀[f:ℕ ⟶ T]. ∀[P:T ⟶ 𝔹].  ||filter(P;map(f;upto(i)))|| < ||filter(P;map(f;upto(j)))|| supposing ↑(P (f i)) 
  supposing i < j
BY
{ (Intros
   THEN ((InstLemma `upto_decomp` [⌜j⌝; ⌜i⌝])⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (RWO "map_append_sq" 0 THENA Auto)
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN (GenConcl ⌜(λx.(x + i)) = addi ∈ (ℕ ⟶ ℕ)⌝⋅ THENA Auto)
   THEN (RWO "length-append" 0 THENA Auto)) }

1
1. T : Type
2. i : ℕ
3. j : ℕ
4. i < j
5. f : ℕ ⟶ T
6. P : T ⟶ 𝔹
7. ↑(P (f i))
8. upto(j) ~ upto(i) @ map(λx.(x + i);upto(j - i))
9. addi : ℕ ⟶ ℕ@i
10. (λx.(x + i)) = addi ∈ (ℕ ⟶ ℕ)
⊢ ||filter(P;map(f;upto(i)))|| < ||filter(P;map(f;upto(i)))|| + ||filter(P;map(f;map(addi;upto(j - i))))||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[i,j:\mBbbN{}].
    \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
        ||filter(P;map(f;upto(i)))||  <  ||filter(P;map(f;upto(j)))||  supposing  \muparrow{}(P  (f  i)) 
    supposing  i  <  j


By

---

Latex:
(Intros
  THEN  ((InstLemma  `upto\_decomp`  [\mkleeneopen{}j\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(\mlambda{}x.(x  +  i))  =  addi\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (RWO  "length-append"  0  THENA  Auto))

---

Home Index