---

Step * 1 1 2 1 1 1 of Lemma sum_switch

.....equality..... 
1. n : ℕ
2. f : ℕn ⟶ ℤ
3. i : ℕn - 1
4. (i, i + 1) ∈ ℕn ⟶ ℕn
⊢ Σ(f[(i, i + 1) (x + i)] | x < 2) = Σ(f[x + i] | x < 2) ∈ ℤ
BY
{ ((RWO "sum-as-primrec" 0 THENA Auto)
   THEN (RWO  "primrec-unroll" 0 THENA Auto)
   THEN Reduce 0
   THEN Unfold `flip` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Repeat (SplitOnConclITE THEN Try (Complete (Auto)))⋅) }

---

Latex:

---

Latex:
.....equality..... 
1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  i  :  \mBbbN{}n  -  1
4.  (i,  i  +  1)  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
\mvdash{}  \mSigma{}(f[(i,  i  +  1)  (x  +  i)]  |  x  <  2)  =  \mSigma{}(f[x  +  i]  |  x  <  2)


By

---

Latex:
((RWO  "sum-as-primrec"  0  THENA  Auto)
  THEN  (RWO    "primrec-unroll"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Unfold  `flip`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Repeat  (SplitOnConclITE  THEN  Try  (Complete  (Auto)))\mcdot{})

---

Home Index