---

Step * 2 1 of Lemma rotate-by-id


1. n : ℕ
2. i : ℕ
3. x : ℕn
4. (i rem n) = 0 ∈ ℤ
⊢ (rotate-by(n;i) x) = ((λx.x) x) ∈ ℕn
BY
{ RepUR ``rotate-by`` 0 }

1
1. n : ℕ
2. i : ℕ
3. x : ℕn
4. (i rem n) = 0 ∈ ℤ
⊢ (x + i rem n) = x ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
3.  x  :  \mBbbN{}n
4.  (i  rem  n)  =  0
\mvdash{}  (rotate-by(n;i)  x)  =  ((\mlambda{}x.x)  x)


By

---

Latex:
RepUR  ``rotate-by``  0

---

Home Index