---

Step * of Lemma cycle-transitive1

∀[n:ℕ]. ∀[L:ℕn List].
  ∀[a,b:ℕ].  ((cycle(L)^b - a L[a]) = L[b] ∈ ℕn) supposing ((a ≤ b) and b < ||L||) supposing no_repeats(ℕn;L)
BY
{ ((Auto THEN GenConcl ⌜(b - a) = k ∈ ℕ⌝⋅ THEN Auto')
   THEN (Subst' b ~ a + k 0 THEN Auto')
   THEN (Assert k < ||L|| - a BY
               Auto')
   THEN MoveToConcl (-1)
   THEN ThinVar `b') }

1
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)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].
    \mforall{}[a,b:\mBbbN{}].    ((cycle(L)\^{}b  -  a  L[a])  =  L[b])  supposing  ((a  \mleq{}  b)  and  b  <  ||L||) 
    supposing  no\_repeats(\mBbbN{}n;L)


By

---

Latex:
((Auto  THEN  GenConcl  \mkleeneopen{}(b  -  a)  =  k\mkleeneclose{}\mcdot{}  THEN  Auto')
  THEN  (Subst'  b  \msim{}  a  +  k  0  THEN  Auto')
  THEN  (Assert  k  <  ||L||  -  a  BY
                          Auto')
  THEN  MoveToConcl  (-1)
  THEN  ThinVar  `b')

---

Home Index