---

Step * of Lemma orbit-transitive

∀[T:Type]. ∀f:T ⟶ T. ∀L:T List.  (∀a∈L.(∀b∈L.∃n:ℕ. ((f^n a) = b ∈ T))) supposing orbit(T;f;L)
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN D -1
   THEN (BLemma `l_all_iff` THEN Auto)
   THEN RepeatFor 2 (D -1)
   THEN (HypSubst' -1 0 THENA Auto)
   THEN ThinVar `a'
   THEN Auto
   THEN RenameVar `j' (-2)
   THEN (BLemma `l_all_iff` THEN Auto)
   THEN RepeatFor 2 (D -1)
   THEN (HypSubst' -1 0 THENA Auto)
   THEN ThinVar `b'
   THEN Auto) }

1
1. [T] : Type
2. f : T ⟶ T
3. L : T List
4. 0 < ||L||
5. no_repeats(T;L)
6. ∀i:ℕ||L||. ((f L[i]) = if (i =z ||L|| - 1) then L[0] else L[i + 1] fi  ∈ T)
7. j : ℕ
8. j < ||L||
9. i : ℕ
10. i < ||L||
⊢ ∃n:ℕ. ((f^n L[j]) = L[i] ∈ T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}L:T  List.    (\mforall{}a\mmember{}L.(\mforall{}b\mmember{}L.\mexists{}n:\mBbbN{}.  ((f\^{}n  a)  =  b)))  supposing  orbit(T;f;L)


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  (BLemma  `l\_all\_iff`  THEN  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  Auto
  THEN  RenameVar  `j'  (-2)
  THEN  (BLemma  `l\_all\_iff`  THEN  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  (HypSubst'  -1  0  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  Auto)

---

Home Index