---

Step * 2 1 of Lemma orbit-decomp2


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. Inj(T;T;f)
6. orbits : T List List
7. (∀orbit∈orbits.0 < ||orbit||
          ∧ no_repeats(T;orbit)
          ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ T))
          ∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
12. ∀i:ℕ||orbits||. ∀j:ℕi.  l_disjoint(T;orbits[j];orbits[i])
13. i : ℕ
14. j : ℕ
15. i < ||orbits||
16. j < ||orbits||
17. ¬(i = j ∈ ℕ)
18. orbits[i] = orbits[j] ∈ (T List)
⊢ False
BY
{ (Assert l_disjoint(T;orbits[j];orbits[j]) BY
         ((Decide i < j THENA Auto)
          THENL [(InstHyp [⌜j⌝;⌜i⌝] (-8)⋅ THEN Auto'); (InstHyp [⌜i⌝;⌜j⌝] (-8)⋅ THEN Auto')]
         )) }

1
1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. finite-type(T)
4. f : T ⟶ T
5. Inj(T;T;f)
6. orbits : T List List
7. (∀orbit∈orbits.0 < ||orbit||
          ∧ no_repeats(T;orbit)
          ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ T))
          ∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))
8. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
9. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
12. ∀i:ℕ||orbits||. ∀j:ℕi.  l_disjoint(T;orbits[j];orbits[i])
13. i : ℕ
14. j : ℕ
15. i < ||orbits||
16. j < ||orbits||
17. ¬(i = j ∈ ℕ)
18. orbits[i] = orbits[j] ∈ (T List)
19. l_disjoint(T;orbits[j];orbits[j])
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  finite-type(T)
4.  f  :  T  {}\mrightarrow{}  T
5.  Inj(T;T;f)
6.  orbits  :  T  List  List
7.  (\mforall{}orbit\mmember{}orbits.0  <  ||orbit||
                    \mwedge{}  no\_repeats(T;orbit)
                    \mwedge{}  (\mforall{}i:\mBbbN{}||orbit||
                              ((f  orbit[i])  =  if  (i  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i  +  1]  fi  ))
                    \mwedge{}  (\mforall{}x\mmember{}orbit.\mforall{}n:\mBbbN{}.  (f\^{}n  x  \mmember{}  orbit)))
8.  \mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
9.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
10.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
11.  \mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
12.  \mforall{}i:\mBbbN{}||orbits||.  \mforall{}j:\mBbbN{}i.    l\_disjoint(T;orbits[j];orbits[i])
13.  i  :  \mBbbN{}
14.  j  :  \mBbbN{}
15.  i  <  ||orbits||
16.  j  <  ||orbits||
17.  \mneg{}(i  =  j)
18.  orbits[i]  =  orbits[j]
\mvdash{}  False


By

---

Latex:
(Assert  l\_disjoint(T;orbits[j];orbits[j])  BY
              ((Decide  i  <  j  THENA  Auto)
                THENL  [(InstHyp  [\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-8)\mcdot{}  THEN  Auto');  (InstHyp  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  (-8)\mcdot{}  THEN  Auto')]
              ))

---

Home Index