---

Step * of Lemma concat_map_upto

∀[T:Type]. ∀f:ℕ ⟶ (T List). ∀t,t':ℕ.  concat(map(f;upto(t))) @ (f t) ≤ concat(map(f;upto(t'))) supposing t < t'
BY
{ (Auto THEN Subst ⌜concat(map(f;upto(t))) @ (f t) ~ concat(map(f;upto(t + 1)))⌝ 0⋅) }

1
.....equality..... 
1. T : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ concat(map(f;upto(t))) @ (f t) ~ concat(map(f;upto(t + 1)))

2
1. [T] : Type
2. f : ℕ ⟶ (T List)@i
3. t : ℕ@i
4. t' : ℕ@i
5. t < t'
⊢ concat(map(f;upto(t + 1))) ≤ concat(map(f;upto(t')))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  (T  List).  \mforall{}t,t':\mBbbN{}.
        concat(map(f;upto(t)))  @  (f  t)  \mleq{}  concat(map(f;upto(t')))  supposing  t  <  t'


By

---

Latex:
(Auto  THEN  Subst  \mkleeneopen{}concat(map(f;upto(t)))  @  (f  t)  \msim{}  concat(map(f;upto(t  +  1)))\mkleeneclose{}  0\mcdot{})

---

Home Index