---

Step * of Lemma cycle-flip-lemma

∀[n:ℕ]. ∀[L:ℕn List].
  (cycle(L) = ((hd(L), hd(tl(L))) o cycle(tl(L))) ∈ (ℕn ⟶ ℕn)) supposing (1 < ||L|| and no_repeats(ℕn;L))
BY
{ (Auto THEN (DVar `L' THEN All Reduce THEN Auto') THEN (DVar `v' THEN All Reduce THEN Auto')⋅) }

1
1. n : ℕ
2. u : ℕn
3. u1 : ℕn
4. v : ℕn List
5. no_repeats(ℕn;[u; [u1 / v]])
6. 1 < (||v|| + 1) + 1
⊢ cycle([u; [u1 / v]]) = ((u, u1) o cycle([u1 / v])) ∈ (ℕn ⟶ ℕn)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].
    (cycle(L)  =  ((hd(L),  hd(tl(L)))  o  cycle(tl(L))))  supposing  (1  <  ||L||  and  no\_repeats(\mBbbN{}n;L))


By

---

Latex:
(Auto  THEN  (DVar  `L'  THEN  All  Reduce  THEN  Auto')  THEN  (DVar  `v'  THEN  All  Reduce  THEN  Auto')\mcdot{})

---

Home Index