---

Step * 1 of Lemma iterated-rotate


1. n : ℕ
2. i : ℤ
3. 0 < i
4. rot(n)^i - 1 = (λx.if x + (i - 1) <z n then x + (i - 1) else (x + (i - 1)) - n fi ) ∈ (ℕn ⟶ ℕn) 
   supposing (i - 1) ≤ n
5. i ≤ n
6. x : ℕn
⊢ (rot(n)^i x) = if x + i <z n then x + i else (x + i) - n fi  ∈ ℕn
BY
{ (D 4 THENA Auto) }

1
1. n : ℕ
2. i : ℤ
3. 0 < i
4. i ≤ n
5. x : ℕn
6. rot(n)^i - 1 = (λx.if x + (i - 1) <z n then x + (i - 1) else (x + (i - 1)) - n fi ) ∈ (ℕn ⟶ ℕn)
⊢ (rot(n)^i x) = if x + i <z n then x + i else (x + i) - n fi  ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbZ{}
3.  0  <  i
4.  rot(n)\^{}i  -  1  =  (\mlambda{}x.if  x  +  (i  -  1)  <z  n  then  x  +  (i  -  1)  else  (x  +  (i  -  1))  -  n  fi  ) 
      supposing  (i  -  1)  \mleq{}  n
5.  i  \mleq{}  n
6.  x  :  \mBbbN{}n
\mvdash{}  (rot(n)\^{}i  x)  =  if  x  +  i  <z  n  then  x  +  i  else  (x  +  i)  -  n  fi 


By

---

Latex:
(D  4  THENA  Auto)

---

Home Index