---

Step * of Lemma int-dot-reduce-dim

∀[as,bs:ℤ List]. ∀[i:ℕ].
  ∀[cs:ℤ List]. (as ⋅ bs ~ as[i] * cs + as\i ⋅ bs\i) supposing ((bs[i] = cs ⋅ bs\i ∈ ℤ) and (||cs|| = (||as|| - 1) ∈ ℤ))\000C 
  supposing i < ||as|| ∧ i < ||bs||
BY
{ (InstLemma  `int-dot-select` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Auto
   THEN HypSubst' (-4) 0
   THEN HypSubst' (-1) 0
   THEN RWW "int-dot-mul-left< int-dot-add-left" 0
   THEN Auto
   THEN RWO "length-int-vec-mul length-list-delete" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as,bs:\mBbbZ{}  List].  \mforall{}[i:\mBbbN{}].
    \mforall{}[cs:\mBbbZ{}  List]
        (as  \mcdot{}  bs  \msim{}  as[i]  *  cs  +  as\mbackslash{}i  \mcdot{}  bs\mbackslash{}i)  supposing  ((bs[i]  =  cs  \mcdot{}  bs\mbackslash{}i)  and  (||cs||  =  (||as||  -  1)))\000C 
    supposing  i  <  ||as||  \mwedge{}  i  <  ||bs||


By

---

Latex:
(InstLemma    `int-dot-select`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Auto
  THEN  HypSubst'  (-4)  0
  THEN  HypSubst'  (-1)  0
  THEN  RWW  "int-dot-mul-left<  int-dot-add-left"  0
  THEN  Auto
  THEN  RWO  "length-int-vec-mul  length-list-delete"  0
  THEN  Auto)

---

Home Index