---

Step * of Lemma int-dot-select

∀[as,bs:ℤ List]. ∀[i:ℕ].  as ⋅ bs ~ (as[i] * bs[i]) + as\i ⋅ bs\i supposing i < ||as|| ∧ i < ||bs||
BY
{ (RepeatFor 2 (InductionOnList)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "select-cons" 0 THENA Auto)
   THEN AutoSplit
   THEN RecUnfold `list-delete` 0
   THEN Reduce 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}].    as  \mcdot{}  bs  \msim{}  (as[i]  *  bs[i])  +  as\mbackslash{}i  \mcdot{}  bs\mbackslash{}i  supposing  i  <  ||as||  \mwedge{}  i  <  ||bs||


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "select-cons"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  RecUnfold  `list-delete`  0
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index