---

Step * 2 of Lemma rotate-by-trivial


1. n : ℕ
2. x : ℕn
3. (rotate-by(n;0) x) = x ∈ ℕn
4. ∀[i:ℕ]. uiff(rotate-by(n;i) = (λx.x) ∈ (ℕn ⟶ ℕn);(i rem n) = 0 ∈ ℤ supposing 0 < n)
⊢ (rotate-by(n;n) x) = x ∈ ℕn
BY
{ ((InstHyp [⌜n⌝] (-1)⋅ THEN Auto)
   THEN (D -1 THENA (Auto THEN BLemma `divides_iff_rem_zero` THEN Auto THEN With ⌜1⌝ (D 0)⋅ THEN Auto))
   THEN HypSubst (-1) 0
   THEN Reduce 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbN{}n
3.  (rotate-by(n;0)  x)  =  x
4.  \mforall{}[i:\mBbbN{}].  uiff(rotate-by(n;i)  =  (\mlambda{}x.x);(i  rem  n)  =  0  supposing  0  <  n)
\mvdash{}  (rotate-by(n;n)  x)  =  x


By

---

Latex:
((InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  THEN  (D  -1
              THENA  (Auto  THEN  BLemma  `divides\_iff\_rem\_zero`  THEN  Auto  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
              )
  THEN  HypSubst  (-1)  0
  THEN  Reduce  0
  THEN  Auto)\mcdot{}

---

Home Index