---

Step * of Lemma rng_sum-int

∀[a,b:ℤ]. ∀[f:{a..b-} ⟶ ℤ].  (Σ(ℤ-rng) a ≤ i < b. f[i]) = Σ(f[a + i] | i < b - a) ∈ ℤ supposing a ≤ b
BY
{ (Auto
   THEN (RepUR ``rng_sum mon_itop`` 0
         THEN (RWO "sum-as-primrec" 0 THENA Auto)
         THEN Assert ⌜∀n:ℕ. ∀a,b:ℤ.
                        ((a ≤ b)
                        ⇒ (b ≤ (a + n))
                        ⇒ (∀f:{a..b-} ⟶ ℤ. (Π(λu,v. (u + v),0) a ≤ i < b. f[i] = primrec(b - a;0;λi,n. (n + f[a + i]))\000C ∈ ℤ)))⌝
         ⋅
         THEN Try (((InstHyp [⌜b - a⌝] (-1)⋅ THENA Complete (Auto')) THEN BHyp -1  THEN Auto))
         THEN All Thin
         THEN InductionOnNat
         THEN Auto
         THEN (RecUnfold `itop` 0
               THEN AutoSplit
               THEN (RWO "primrec-unroll" 0 THENA Auto)
               THEN AutoSplit
               THEN Auto'
               THEN RWO "3" 0
               THEN Auto
               THEN Auto')⋅)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[f:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(\mBbbZ{}-rng)  a  \mleq{}  i  <  b.  f[i])  =  \mSigma{}(f[a  +  i]  |  i  <  b  -  a)  supposing  a  \mleq{}  b


By

---

Latex:
(Auto
  THEN  (RepUR  ``rng\_sum  mon\_itop``  0
              THEN  (RWO  "sum-as-primrec"  0  THENA  Auto)
              THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbZ{}.
                                            ((a  \mleq{}  b)
                                            {}\mRightarrow{}  (b  \mleq{}  (a  +  n))
                                            {}\mRightarrow{}  (\mforall{}f:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}
                                                        (\mPi{}(\mlambda{}u,v.  (u  +  v),0)  a  \mleq{}  i  <  b.  f[i]  =  primrec(b  -  a;0;\mlambda{}i,n.  (n  +  f[a  +  i\000C])))))\mkleeneclose{}\mcdot{}
              THEN  Try  (((InstHyp  [\mkleeneopen{}b  -  a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Complete  (Auto'))  THEN  BHyp  -1    THEN  Auto))
              THEN  All  Thin
              THEN  InductionOnNat
              THEN  Auto
              THEN  (RecUnfold  `itop`  0
                          THEN  AutoSplit
                          THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                          THEN  AutoSplit
                          THEN  Auto'
                          THEN  RWO  "3"  0
                          THEN  Auto
                          THEN  Auto')\mcdot{})\mcdot{}
  )

---

Home Index