---

Step * 1 1 2 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 ─→ ℚ@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]||))))))
∈ ℚ
BY
{ OnMaybeHyp 4 (\h. ((InstHyp [⌈n - 1⌉;⌈λx.(F (x + 1))⌉;⌈λx.(G (x + 1))⌉;⌈v⌉] h⋅ THENA Auto')
                     THEN All Reduce
                     THEN HypSubst' -1 0
                     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 ─→ ℚ@i
6. G : ℕn ─→ ℚ@i
7. u : ℚ
8. v : ℚ List
9. (||v|| + 1) ≤ n@i
10. ¬(||v|| ≤ 0)
11. weighted-sum(v;λx.((a * (F (x + 1))) + (b * (G (x + 1)))))
= ((a * weighted-sum(v;λx.(F (x + 1)))) + (b * weighted-sum(v;λx.(G (x + 1)))))
∈ ℚ
⊢ ((0 + (((a * (F 0)) + (b * (G 0))) * u))
+ (a * weighted-sum(v;λx.(F (x + 1))))
+ (b * weighted-sum(v;λx.(G (x + 1)))))
= ((a * ((0 + ((F 0) * u)) + weighted-sum(v;λi.(F (i + 1)))))
  + (b * ((0 + ((G 0) * u)) + weighted-sum(v;λi.(G (i + 1))))))
∈ ℚ

---

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
10.  \mneg{}(||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

OnMaybeHyp  4  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(F  (x  +  1))\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(G  (x  +  1))\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  h\mcdot{}  THENA  Auto')
                                      THEN  All  Reduce
                                      THEN  HypSubst'  -1  0
                                      THEN  Auto'))

---

Home Index