---

Step * 1 1 2 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 ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. u : ℚ
8. v : ℚ List
9. ||[u / v]|| ≤ n@i
⊢ (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
{ (Decide ||v|| ≤ 0 THENA 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 ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. u : ℚ
8. v : ℚ List
9. ||[u / v]|| ≤ n@i
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]||))))))
∈ ℚ

2
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 ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. u : ℚ
8. v : ℚ List
9. ||[u / v]|| ≤ n@i
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]||))))))
∈ ℚ

---

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{}@i
6.  G  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}@i
7.  u  :  \mBbbQ{}
8.  v  :  \mBbbQ{}  List
9.  ||[u  /  v]||  \mleq{}  n@i
\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

(Decide  ||v||  \mleq{}  0  THENA  Auto)

---

Home Index