---

Step * 1 1 of Lemma iterated-rotate


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
BY
{ (Unfold `fun_exp` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Fold `fun_exp` 0
   THEN SplitOnConclITE
   THEN Auto
   THEN Reduce 0
   THEN (HypSubst (-2) 0 THENA TACTIC:(SplitOnConclITE THEN Auto THEN Auto'))
   THEN (RepUR ``rotate`` 0
         THEN AutoBoolCase ⌜x + (i - 1) <z n⌝⋅
         THEN AutoBoolCase ⌜x + i <z n⌝⋅
         THEN SplitOnConclITE
         THEN Auto')⋅)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `fun\_exp`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Fold  `fun\_exp`  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  Reduce  0
  THEN  (HypSubst  (-2)  0  THENA  TACTIC:(SplitOnConclITE  THEN  Auto  THEN  Auto'))
  THEN  (RepUR  ``rotate``  0
              THEN  AutoBoolCase  \mkleeneopen{}x  +  (i  -  1)  <z  n\mkleeneclose{}\mcdot{}
              THEN  AutoBoolCase  \mkleeneopen{}x  +  i  <z  n\mkleeneclose{}\mcdot{}
              THEN  SplitOnConclITE
              THEN  Auto')\mcdot{})\mcdot{}

---

Home Index