---

Step * of Lemma iterated-rotate

∀[n,i:ℕ].  rot(n)^i = (λx.if x + i <z n then x + i else (x + i) - n fi ) ∈ (ℕn ⟶ ℕn) supposing i ≤ n
BY
{ ((D 0 THENA Auto)
   THEN InductionOnNat
   THEN Reduce 0
   THEN Auto
   THEN Ext
   THEN Reduce 0
   THEN TACTIC:(Try (Complete (Auto)) THEN Try (Complete ((Try (EqCD) THEN Try (SplitOnConclITE) THEN Auto'))))) }

1
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

---

Latex:

---

Latex:
\mforall{}[n,i:\mBbbN{}].    rot(n)\^{}i  =  (\mlambda{}x.if  x  +  i  <z  n  then  x  +  i  else  (x  +  i)  -  n  fi  )  supposing  i  \mleq{}  n


By

---

Latex:
((D  0  THENA  Auto)
  THEN  InductionOnNat
  THEN  Reduce  0
  THEN  Auto
  THEN  Ext
  THEN  Reduce  0
  THEN  TACTIC:(Try  (Complete  (Auto))
                            THEN  Try  (Complete  ((Try  (EqCD)  THEN  Try  (SplitOnConclITE)  THEN  Auto')))
                            ))

---

Home Index