---

Step * 1 of Lemma weighted-sum-split

.....subterm..... T:t
2:n
1. p : ℚ List
2. q : ℚ List
3. F : ℕ||p @ q|| ─→ ℚ
4. Σ0 ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= (Σ0 ≤ j < ||p||. (F j) * p @ q[j] + Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j])
∈ ℚ
⊢ Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j] = Σ0 ≤ i < ||q||. (F (i + ||p||)) * q[i] ∈ ℚ
BY
{ (Reduce 0
   THEN (Subst' Σ0 ≤ i < ||q||. (F (i + ||p||)) * q[i]
         = Σ0 + ||p|| ≤ i < ||q|| + ||p||. (F ((i - ||p||) + ||p||)) * q[i - ||p||]
         ∈ ℚ 0
         THENA Auto'
         )
   ) }

1
.....equality..... 
1. p : ℚ List
2. q : ℚ List
3. F : ℕ||p @ q|| ─→ ℚ
4. Σ0 ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= (Σ0 ≤ j < ||p||. (F j) * p @ q[j] + Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j])
∈ ℚ
⊢ Σ0 ≤ i < ||q||. (F (i + ||p||)) * q[i] = Σ0 + ||p|| ≤ i < ||q|| + ||p||. (F ((i - ||p||) + ||p||)) * q[i - ||p||] ∈ ℚ

2
1. p : ℚ List
2. q : ℚ List
3. F : ℕ||p @ q|| ─→ ℚ
4. Σ0 ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= (Σ0 ≤ j < ||p||. (F j) * p @ q[j] + Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j])
∈ ℚ
⊢ Σ||p|| ≤ j < ||p|| + ||q||. (F j) * p @ q[j]
= Σ0 + ||p|| ≤ i < ||q|| + ||p||. (F ((i - ||p||) + ||p||)) * q[i - ||p||]
∈ ℚ

---

Latex:


.....subterm.....  T:t
2:n
1.  p  :  \mBbbQ{}  List
2.  q  :  \mBbbQ{}  List
3.  F  :  \mBbbN{}||p  @  q||  {}\mrightarrow{}  \mBbbQ{}
4.  \mSigma{}0  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j]
=  (\mSigma{}0  \mleq{}  j  <  ||p||.  (F  j)  *  p  @  q[j]  +  \mSigma{}||p||  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j])
\mvdash{}  \mSigma{}||p||  \mleq{}  j  <  ||p||  +  ||q||.  (F  j)  *  p  @  q[j]  =  \mSigma{}0  \mleq{}  i  <  ||q||.  (F  (i  +  ||p||))  *  q[i]


By

(Reduce  0
  THEN  (Subst'  \mSigma{}0  \mleq{}  i  <  ||q||.  (F  (i  +  ||p||))  *  q[i]
              =  \mSigma{}0  +  ||p||  \mleq{}  i  <  ||q||  +  ||p||.  (F  ((i  -  ||p||)  +  ||p||))  *  q[i  -  ||p||]  0
              THENA  Auto'
              )
  )

---

Home Index