---

Step * 2 2 1 of Lemma fps-product-upto


1. k : ℕ+
⊢ map(λx.(x + (-1));[1, k)) ~ [0, k - 1)
BY
{ xxx(RWO "from-upto-shift" 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  map(\mlambda{}x.(x  +  (-1));[1,  k))  \msim{}  [0,  k  -  1)


By

---

Latex:
xxx(RWO  "from-upto-shift"  0  THEN  Auto)xxx

---

Home Index