---

Step * 1 1 2 1 1 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
10. ||v|| ≤ 0
⊢ (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]||))))))
∈ ℚ
BY
{ (DVar `v' THEN All Reduce  THEN Auto') }

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. 1 ≤ n
9. 0 ≤ 0
⊢ ((0 + (((a * (F 0)) + (b * (G 0))) * u)) + 0) = ((a * ((0 + ((F 0) * u)) + 0)) + (b * ((0 + ((G 0) * u)) + 0))) ∈ ℚ

---

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
10.  ||v||  \mleq{}  0
\mvdash{}  (weighted-sum([u];\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
+  weighted-sum(v;\mlambda{}i.((\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))  (i  +  ||[u]||))))
=  ((a  *  (weighted-sum([u];F)  +  weighted-sum(v;\mlambda{}i.(F  (i  +  ||[u]||)))))
    +  (b  *  (weighted-sum([u];G)  +  weighted-sum(v;\mlambda{}i.(G  (i  +  ||[u]||))))))


By

---

Latex:
(DVar  `v'  THEN  All  Reduce    THEN  Auto')

---

Home Index