---

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

.....antecedent..... 
1. ll : Top List+ List
⊢ (∀x∈map(λl.||l||;ll).1 ≤ x)
BY
{ (BLemma `l_all_iff`
   THEN Auto
   THEN (RepeatFor 2 (D (-1))
         THEN ((RWO "select-map" (-1) THENM Reduce (-1) THENM HypSubst' (-1) 0) THENA Auto)
         THEN GenConclAtAddr [2;1]
         THEN Auto
         THEN D (-2)
         THEN Auto)⋅) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  ll  :  Top  List\msupplus{}  List
\mvdash{}  (\mforall{}x\mmember{}map(\mlambda{}l.||l||;ll).1  \mleq{}  x)


By

---

Latex:
(BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  (RepeatFor  2  (D  (-1))
              THEN  ((RWO  "select-map"  (-1)  THENM  Reduce  (-1)  THENM  HypSubst'  (-1)  0)  THENA  Auto)
              THEN  GenConclAtAddr  [2;1]
              THEN  Auto
              THEN  D  (-2)
              THEN  Auto)\mcdot{})

---

Home Index