---

Step * 1 of Lemma length-concat-lower-bound


1. ll : Top List+ List
⊢ ||ll|| ≤ l_sum(map(λl.||l||;ll))
BY
{ (InstLemma `l_sum-lower-bound` [⌜1⌝;⌜map(λl.||l||;ll)⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. ll : Top List+ List
⊢ (∀x∈map(λl.||l||;ll).1 ≤ x)

---

Latex:

---

Latex:

1.  ll  :  Top  List\msupplus{}  List
\mvdash{}  ||ll||  \mleq{}  l\_sum(map(\mlambda{}l.||l||;ll))


By

---

Latex:
(InstLemma  `l\_sum-lower-bound`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}map(\mlambda{}l.||l||;ll)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index