---

Step * 1 of Lemma sum_split


1. n : ℕ
2. f : ℕn ⟶ ℤ
3. m : ℕn + 1
4. primrec(n;0;λj,x. (x + f[j])) ~ primrec(n - m;primrec(m;0;λj,x. (x + f[j]));λi,t. ((λj,x. (x + f[j])) (i + m) t))
5. v : ℤ
6. primrec(m;0;λj,x. (x + f[j])) = v ∈ ℤ
7. k : ℕ
8. (n - m) = k ∈ ℕ
⊢ primrec(k;v;λi,t. (t + f[i + m])) = (v + primrec(k;0;λj,x. (x + f[j + m]))) ∈ ℤ
BY
{ ((Assert k ≤ (n - m) BY
          Auto)
   THEN MoveToConcl (-1)
   THEN Thin (-1)
   THEN NatInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  m  :  \mBbbN{}n  +  1
4.  primrec(n;0;\mlambda{}j,x.  (x  +  f[j]))  \msim{}  primrec(n 
-  m;primrec(m;0;\mlambda{}j,x.  (x  +  f[j]));\mlambda{}i,t.  ((\mlambda{}j,x.  (x  +  f[j]))  (i  +  m)  t))
5.  v  :  \mBbbZ{}
6.  primrec(m;0;\mlambda{}j,x.  (x  +  f[j]))  =  v
7.  k  :  \mBbbN{}
8.  (n  -  m)  =  k
\mvdash{}  primrec(k;v;\mlambda{}i,t.  (t  +  f[i  +  m]))  =  (v  +  primrec(k;0;\mlambda{}j,x.  (x  +  f[j  +  m])))


By

---

Latex:
((Assert  k  \mleq{}  (n  -  m)  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  Thin  (-1)
  THEN  NatInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index