---

Step * of Lemma length-concat-lower-bound

∀[ll:Top List+ List]. (||ll|| ≤ ||concat(ll)||)
BY
{ ((Auto THEN RWO "length-concat" 0) THEN Auto) }

1
1. ll : Top List+ List
⊢ ||ll|| ≤ l_sum(map(λl.||l||;ll))

---

Latex:

---

Latex:
\mforall{}[ll:Top  List\msupplus{}  List].  (||ll||  \mleq{}  ||concat(ll)||)


By

---

Latex:
((Auto  THEN  RWO  "length-concat"  0)  THEN  Auto)

---

Home Index