---

Step * of Lemma weighted-sum-split

∀[p,q:ℚ List]. ∀[F:ℕ||p @ q|| ─→ ℚ].
  (weighted-sum(p @ q;F) = (weighted-sum(p;F) + weighted-sum(q;λi.(F (i + ||p||)))) ∈ ℚ)
BY
{ (Unfold `weighted-sum` 0
   THEN Auto'
   THEN (InstLemma `sum_split_q` [⌈0⌉;⌈||p||⌉;⌈||p|| + ||q||⌉;⌈λi.((F i) * p @ q[i])⌉]⋅ THENA Auto')
   THEN (ReduceSOAps (-1))
   THEN (HypSubst' -1 0 THENA (Reduce 0 THEN Auto'))
   THEN EqCD
   THEN Auto
   THEN Try (Complete ((EqCD THEN Auto THEN RWO "select_append_front" 0 THEN Auto')))) }

1
.....subterm..... T:t
2:n
1. p : ℚ List
2. q : ℚ List
3. F : ℕ||p @ q|| ─→ ℚ
4. Σ0 ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= (Σ0 ≤ j < ||p||. (F j) * p @ q[j] + Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j])
∈ ℚ
⊢ Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j] = Σ0 ≤ i < ||q||. (F (i + ||p||)) * q[i] ∈ ℚ

---

Latex:


\mforall{}[p,q:\mBbbQ{}  List].  \mforall{}[F:\mBbbN{}||p  @  q||  {}\mrightarrow{}  \mBbbQ{}].
    (weighted-sum(p  @  q;F)  =  (weighted-sum(p;F)  +  weighted-sum(q;\mlambda{}i.(F  (i  +  ||p||)))))


By

(Unfold  `weighted-sum`  0
  THEN  Auto'
  THEN  (InstLemma  `sum\_split\_q`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}||p||\mkleeneclose{};\mkleeneopen{}||p||  +  ||q||\mkleeneclose{};\mkleeneopen{}\mlambda{}i.((F  i)  *  p  @  q[i])\mkleeneclose{}]\mcdot{}  THENA  Auto')
  THEN  (ReduceSOAps  (-1))
  THEN  (HypSubst'  -1  0  THENA  (Reduce  0  THEN  Auto'))
  THEN  EqCD
  THEN  Auto
  THEN  Try  (Complete  ((EqCD  THEN  Auto  THEN  RWO  "select\_append\_front"  0  THEN  Auto'))))

---

Home Index