---

Step * 1 2 of Lemma weighted-sum-linear


1. a : ℚ
2. b : ℚ
3. ∀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))) ∈ ℚ))
⊢ ∀[p:ℚ List]. ∀[F,G:ℕ||p|| ⟶ ℚ].
    (weighted-sum(p;λx.((a * (F x)) + (b * (G x)))) = ((a * weighted-sum(p;F)) + (b * weighted-sum(p;G))) ∈ ℚ)
BY
{ xxx((D 0 THENA Auto)
      THEN ((InstHyp [⌜||p||⌝] (-2))⋅ THENA Auto)
      THEN RepeatFor 2 (ParallelLast)
      THEN (InstHyp [⌜p⌝] (-1))⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  \mforall{}n:\mBbbN{}.  \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)))))
\mvdash{}  \mforall{}[p:\mBbbQ{}  List].  \mforall{}[F,G:\mBbbN{}||p||  {}\mrightarrow{}  \mBbbQ{}].
        (weighted-sum(p;\mlambda{}x.((a  *  (F  x))  +  (b  *  (G  x))))
        =  ((a  *  weighted-sum(p;F))  +  (b  *  weighted-sum(p;G))))


By

---

Latex:
xxx((D  0  THENA  Auto)
        THEN  ((InstHyp  [\mkleeneopen{}||p||\mkleeneclose{}]  (-2))\mcdot{}  THENA  Auto)
        THEN  RepeatFor  2  (ParallelLast)
        THEN  (InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  (-1))\mcdot{}
        THEN  Auto)xxx

---

Home Index