---

Step * 2 of Lemma iterate-rotate-by

.....upcase..... 
1. n : ℕ
2. i : ℕ
3. k : ℤ
4. 0 < k
5. rotate-by(n;i)^k - 1 = rotate-by(n;(k - 1) * i) ∈ (ℕn ⟶ ℕn)
⊢ rotate-by(n;i)^k = rotate-by(n;k * i) ∈ (ℕn ⟶ ℕn)
BY
{ ((RWO "fun_exp_unroll_1" 0 THENA Auto) THEN Reduce 0 THEN (HypSubst' (-1) 0 THENA Auto)) }

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

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}
3.  k  :  \mBbbZ{}
4.  0  <  k
5.  rotate-by(n;i)\^{}k  -  1  =  rotate-by(n;(k  -  1)  *  i)
\mvdash{}  rotate-by(n;i)\^{}k  =  rotate-by(n;k  *  i)


By

---

Latex:
((RWO  "fun\_exp\_unroll\_1"  0  THENA  Auto)  THEN  Reduce  0  THEN  (HypSubst'  (-1)  0  THENA  Auto))

---

Home Index