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