---

Step * of Lemma length_concat

∀[T:Type]. ∀[ll:T List List].  (||concat(ll)|| = Σ(||ll[i]|| | i < ||ll||) ∈ ℤ)
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "concat-cons" 0 THENA Auto)
   THEN (RWO "length_append" 0 THENA Auto)
   THEN HypSubst' (-1) 0
   THEN (InstLemma `sum_split` [⌜||v|| + 1⌝;⌜λ2i.||[u / v][i]||⌝;⌜1⌝]⋅ THENA (Auto THEN Thin (-1) THEN Auto))
   THEN HypSubst' (-1) 0
   THEN Thin (-1)
   THEN EqCD
   THEN Try (RepeatFor 2 ((EqCD THEN Auto)))
   THEN RWO "sum1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[ll:T  List  List].    (||concat(ll)||  =  \mSigma{}(||ll[i]||  |  i  <  ||ll||))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "concat-cons"  0  THENA  Auto)
  THEN  (RWO  "length\_append"  0  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  (InstLemma  `sum\_split`  [\mkleeneopen{}||v||  +  1\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.||[u  /  v][i]||\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Thin  (-1)  THEN  Auto)
              )
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1)
  THEN  EqCD
  THEN  Try  (RepeatFor  2  ((EqCD  THEN  Auto)))
  THEN  RWO  "sum1"  0
  THEN  Auto)

---

Home Index