---

Step * of Lemma rng_prod_plus

∀[r:CRng]. ∀[n:ℕ]. ∀[F,G:ℕn ⟶ |r|].
  ((Π(r) 0 
         ≤ i 
         < n
     F[i] +r G[i])
  = Σ{r} p ∈ functions-list(n;2). (Π(r) 0 
                                        ≤ i 
                                        < n
                                    if (p i =z 0) then F[i] else G[i] fi )
  ∈ |r|)
BY
{ ((InductionOnNat THEN Auto)
   THENL [(Reduce 0 THEN (RWO "functions-list-0" 0 THENA Auto) THEN Reduce 0 THEN Auto)
         ; ((RWO "rng_prod_unroll_hi" 0 THENA Auto) THEN (RWO "-3" 0 THENA Auto) THEN Thin (-3))]
) }

1
1. r : CRng
2. n : ℤ
3. 0 < n
4. F : ℕn ⟶ |r|
5. G : ℕn ⟶ |r|
⊢ (Σ{r} p ∈ functions-list(n - 1;2). (Π(r) 0 
                                           ≤ i 
                                           < n - 1
                                       if (p i =z 0) then F[i] else G[i] fi ) 
   * 
   (F[n - 1] +r G[n - 1]))
= Σ{r} p ∈ functions-list(n;2). ((Π(r) 0 
                                       ≤ i 
                                       < n - 1
                                   if (p i =z 0) then F[i] else G[i] fi ) 
                                 * 
                                 if (p (n - 1) =z 0) then F[n - 1] else G[n - 1] fi )
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}].  \mforall{}[F,G:\mBbbN{}n  {}\mrightarrow{}  |r|].
    ((\mPi{}(r)  0 
                  \mleq{}  i 
                  <  n
          F[i]  +r  G[i])
    =  \mSigma{}\{r\}  p  \mmember{}  functions-list(n;2).  (\mPi{}(r)  0 
                                                                                \mleq{}  i 
                                                                                <  n
                                                                        if  (p  i  =\msubz{}  0)  then  F[i]  else  G[i]  fi  ))


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THENL  [(Reduce  0  THEN  (RWO  "functions-list-0"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)
              ;  ((RWO  "rng\_prod\_unroll\_hi"  0  THENA  Auto)  THEN  (RWO  "-3"  0  THENA  Auto)  THEN  Thin  (-3))]
)

---

Home Index