---

Step * 1 1 1 1 of Lemma sum_switch


1. n : ℕ
2. f : ℕn ⟶ ℤ
3. i : ℕn - 1
4. (i, i + 1) ∈ ℕn ⟶ ℕn
5. i1 : ℕi@i
⊢ f[(i, i + 1) i1] = f[i1] ∈ ℤ
BY
{ TACTIC:(Unfold `flip` 0 THEN Reduce 0 THEN Repeat (SplitOnConclITE THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
3.  i  :  \mBbbN{}n  -  1
4.  (i,  i  +  1)  \mmember{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
5.  i1  :  \mBbbN{}i@i
\mvdash{}  f[(i,  i  +  1)  i1]  =  f[i1]


By

---

Latex:
TACTIC:(Unfold  `flip`  0  THEN  Reduce  0  THEN  Repeat  (SplitOnConclITE  THEN  Auto)\mcdot{})

---

Home Index