---

Step * of Lemma rotate-by-id

∀[n,i:ℕ].  uiff(rotate-by(n;i) = (λx.x) ∈ (ℕn ⟶ ℕn);(i rem n) = 0 ∈ ℤ supposing 0 < n)
BY
{ xxxxxxAutoxxxxxx }

1
1. n : ℕ
2. i : ℕ
3. rotate-by(n;i) = (λx.x) ∈ (ℕn ⟶ ℕn)
4. 0 < n
⊢ (i rem n) = 0 ∈ ℤ

2
1. n : ℕ
2. i : ℕ
3. (i rem n) = 0 ∈ ℤ supposing 0 < n
⊢ rotate-by(n;i) = (λx.x) ∈ (ℕn ⟶ ℕn)

---

Latex:

---

Latex:
\mforall{}[n,i:\mBbbN{}].    uiff(rotate-by(n;i)  =  (\mlambda{}x.x);(i  rem  n)  =  0  supposing  0  <  n)


By

---

Latex:
xxxxxxAutoxxxxxx

---

Home Index