---

Step * 1 1 1 1 1 of Lemma involution-with-unique-fixpoint


1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. ∀x,y:T.  (((f x) = x ∈ T) ⇒ ((f y) = y ∈ T) ⇒ (x = y ∈ T))
7. x : T
8. (f x) = x ∈ T
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
12. no_repeats(T List;orbits)
13. n = Σ(||orbits[i]|| | i < ||orbits||) ∈ ℤ
14. ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o)
15. j : ℕ||orbits||
16. (x ∈ orbits[j])
17. Σ(||orbits[x]|| | x < ||orbits||)
= (||orbits[j]|| + Σ(if (x =z j) then 0 else ||orbits[x]|| fi  | x < ||orbits||))
∈ ℤ
⊢ (n rem 2) = 1 ∈ ℤ
BY
{ Assert ⌜∀x:ℕ||orbits||. (||orbits[x]|| = if (x =z j) then 1 else 2 fi  ∈ ℤ)⌝⋅ }

1
.....assertion..... 
1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. ∀x,y:T.  (((f x) = x ∈ T) ⇒ ((f y) = y ∈ T) ⇒ (x = y ∈ T))
7. x : T
8. (f x) = x ∈ T
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
12. no_repeats(T List;orbits)
13. n = Σ(||orbits[i]|| | i < ||orbits||) ∈ ℤ
14. ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o)
15. j : ℕ||orbits||
16. (x ∈ orbits[j])
17. Σ(||orbits[x]|| | x < ||orbits||)
= (||orbits[j]|| + Σ(if (x =z j) then 0 else ||orbits[x]|| fi  | x < ||orbits||))
∈ ℤ
⊢ ∀x:ℕ||orbits||. (||orbits[x]|| = if (x =z j) then 1 else 2 fi  ∈ ℤ)

2
1. n : ℕ
2. T : Type
3. T ~ ℕn
4. f : T ⟶ T
5. ∀x:T. ((f (f x)) = x ∈ T)
6. ∀x,y:T.  (((f x) = x ∈ T) ⇒ ((f y) = y ∈ T) ⇒ (x = y ∈ T))
7. x : T
8. (f x) = x ∈ T
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
12. no_repeats(T List;orbits)
13. n = Σ(||orbits[i]|| | i < ||orbits||) ∈ ℤ
14. ∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o)
15. j : ℕ||orbits||
16. (x ∈ orbits[j])
17. Σ(||orbits[x]|| | x < ||orbits||)
= (||orbits[j]|| + Σ(if (x =z j) then 0 else ||orbits[x]|| fi  | x < ||orbits||))
∈ ℤ
18. ∀x:ℕ||orbits||. (||orbits[x]|| = if (x =z j) then 1 else 2 fi  ∈ ℤ)
⊢ (n rem 2) = 1 ∈ ℤ

---

Latex:

---

Latex:

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.  \mforall{}x,y:T.    (((f  x)  =  x)  {}\mRightarrow{}  ((f  y)  =  y)  {}\mRightarrow{}  (x  =  y))
7.  x  :  T
8.  (f  x)  =  x
9.  orbits  :  T  List  List
10.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
11.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
12.  no\_repeats(T  List;orbits)
13.  n  =  \mSigma{}(||orbits[i]||  |  i  <  ||orbits||)
14.  \mforall{}o:T  List.  (||o||  =  1)  \mvee{}  (||o||  =  2)  supposing  orbit(T;f;o)
15.  j  :  \mBbbN{}||orbits||
16.  (x  \mmember{}  orbits[j])
17.  \mSigma{}(||orbits[x]||  |  x  <  ||orbits||)
=  (||orbits[j]||  +  \mSigma{}(if  (x  =\msubz{}  j)  then  0  else  ||orbits[x]||  fi    |  x  <  ||orbits||))
\mvdash{}  (n  rem  2)  =  1


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}x:\mBbbN{}||orbits||.  (||orbits[x]||  =  if  (x  =\msubz{}  j)  then  1  else  2  fi  )\mkleeneclose{}\mcdot{}

---

Home Index