---

Step * 1 1 2 of Lemma weighted-sum-linear


1. a : ℚ
2. b : ℚ
3. n : ℕ
4. ∀n:ℕn. ∀F,G:ℕn ⟶ ℚ. ∀p:ℚ List.
     ((||p|| ≤ n)
     ⇒ (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ))
5. F : ℕn ⟶ ℚ
6. G : ℕn ⟶ ℚ
7. u : ℚ
8. v : ℚ List
9. ||[u / v]|| ≤ n
⊢ weighted-sum([u / v];λx.((a * (F x)) + (b * (G x))))
= ((a * weighted-sum([u / v];F)) + (b * weighted-sum([u / v];G)))
∈ ℚ
BY
{ xxx(Subst' [u / v] ~ [u] @ v 0
      THEN Try (Complete ((Reduce 0 THEN Trivial)))
      THEN (RWO "weighted-sum-split" 0 THENA (Auto' THEN All Reduce THEN Auto')))xxx }

1
1. a : ℚ
2. b : ℚ
3. n : ℕ
4. ∀n:ℕn. ∀F,G:ℕn ⟶ ℚ. ∀p:ℚ List.
     ((||p|| ≤ n)
     ⇒ (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ))
5. F : ℕn ⟶ ℚ
6. G : ℕn ⟶ ℚ
7. u : ℚ
8. v : ℚ List
9. ||[u / v]|| ≤ n
⊢ (weighted-sum([u];λx.((a * (F x)) + (b * (G x))))
+ weighted-sum(v;λi.((λx.((a * (F x)) + (b * (G x)))) (i + ||[u]||))))
= ((a * (weighted-sum([u];F) + weighted-sum(v;λi.(F (i + ||[u]||)))))
  + (b * (weighted-sum([u];G) + weighted-sum(v;λi.(G (i + ||[u]||))))))
∈ ℚ

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  n  :  \mBbbN{}
4.  \mforall{}n:\mBbbN{}n.  \mforall{}F,G:\mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}.  \mforall{}p:\mBbbQ{}  List.
          ((||p||  \mleq{}  n)
          {}\mRightarrow{}  (weighted-sum(p;\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
                =  ((a  *  weighted-sum(p;F))  +  (b  *  weighted-sum(p;G)))))
5.  F  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}
6.  G  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}
7.  u  :  \mBbbQ{}
8.  v  :  \mBbbQ{}  List
9.  ||[u  /  v]||  \mleq{}  n
\mvdash{}  weighted-sum([u  /  v];\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
=  ((a  *  weighted-sum([u  /  v];F))  +  (b  *  weighted-sum([u  /  v];G)))


By

---

Latex:
xxx(Subst'  [u  /  v]  \msim{}  [u]  @  v  0
        THEN  Try  (Complete  ((Reduce  0  THEN  Trivial)))
        THEN  (RWO  "weighted-sum-split"  0  THENA  (Auto'  THEN  All  Reduce  THEN  Auto')))xxx

---

Home Index