---

Step * 2 1 1 1 1 1 1 of Lemma involution-has-fixpoint

.....aux..... 
1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. (n rem 2) = 1 ∈ ℤ
7. orbits : T List List
8. (∀o∈orbits.orbit(T;f;o))
9. ∀a:T. (∃o∈orbits. (a ∈ o))
10. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
11. no_repeats(T List;orbits)
12. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
13. ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o)
14. ∀i:ℕ||orbits||. (¬(||orbits[i]|| = 1 ∈ ℤ))
15. i : ℕ||orbits||
⊢ ||orbits[i]|| = 2 ∈ ℤ
BY
{ ((InstHyp [⌜orbits[i]⌝] (-3)⋅ THEN Auto) THEN D -1 THEN Auto) }

1
1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. (n rem 2) = 1 ∈ ℤ
7. orbits : T List List
8. (∀o∈orbits.orbit(T;f;o))
9. ∀a:T. (∃o∈orbits. (a ∈ o))
10. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
11. no_repeats(T List;orbits)
12. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
13. ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o)
14. ∀i:ℕ||orbits||. (¬(||orbits[i]|| = 1 ∈ ℤ))
15. i : ℕ||orbits||
16. ||orbits[i]|| = 1 ∈ ℤ
⊢ ||orbits[i]|| = 2 ∈ ℤ

---

Latex:

---

Latex:
.....aux..... 
1.  n  :  \mBbbN{}
2.  T  :  Type
3.  T  \msim{}  \mBbbN{}n
4.  f  :  T  {}\mrightarrow{}  T
5.  \mforall{}x:T.  ((f  (f  x))  =  x)
6.  (n  rem  2)  =  1
7.  orbits  :  T  List  List
8.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
9.  \mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o))
10.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
11.  no\_repeats(T  List;orbits)
12.  n  =  l\_sum(map(\mlambda{}o.||o||;orbits))
13.  \mforall{}o:T  List.  (||o||  =  1)  \mvee{}  (||o||  =  2)  supposing  orbit(T;f;o)
14.  \mforall{}i:\mBbbN{}||orbits||.  (\mneg{}(||orbits[i]||  =  1))
15.  i  :  \mBbbN{}||orbits||
\mvdash{}  ||orbits[i]||  =  2


By

---

Latex:
((InstHyp  [\mkleeneopen{}orbits[i]\mkleeneclose{}]  (-3)\mcdot{}  THEN  Auto)  THEN  D  -1  THEN  Auto)

---

Home Index