---

Step * 1 of Lemma cycle-transitive1


1. n : ℕ
2. L : ℕn List
3. no_repeats(ℕn;L)
4. a : ℕ
5. k : ℕ
⊢ k < ||L|| - a ⇒ ((cycle(L)^k L[a]) = L[a + k] ∈ ℕn)
BY
{ (NatInd (-1)
   THEN RW funexpC 0
   THEN Auto
   THEN SplitOnConclITE
   THEN Auto
   THEN Reduce 0
   THEN D -3
   THEN Auto
   THEN (HypSubst' (-1) 0 THEN Auto')
   THEN RWO "apply-cycle-member" 0
   THEN Auto'
   THEN SplitOnConclITE
   THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  L  :  \mBbbN{}n  List
3.  no\_repeats(\mBbbN{}n;L)
4.  a  :  \mBbbN{}
5.  k  :  \mBbbN{}
\mvdash{}  k  <  ||L||  -  a  {}\mRightarrow{}  ((cycle(L)\^{}k  L[a])  =  L[a  +  k])


By

---

Latex:
(NatInd  (-1)
  THEN  RW  funexpC  0
  THEN  Auto
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  Reduce  0
  THEN  D  -3
  THEN  Auto
  THEN  (HypSubst'  (-1)  0  THEN  Auto')
  THEN  RWO  "apply-cycle-member"  0
  THEN  Auto'
  THEN  SplitOnConclITE
  THEN  Auto')

---

Home Index