---

Step * 1 2 1 of Lemma eqmod-by-orbits


1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T}  ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
⊢ ℕ||filter(λo.(||o|| =z 1);orbits)|| ~ {x:T| (f x) = x ∈ T} 
BY
{ TACTIC:Assert ⌜filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)}  List⌝⋅ }

1
.....assertion..... 
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T}  ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
⊢ filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)}  List

2
1. n : ℕ
2. k : ℕ
3. p : ℕ
4. T : Type
5. f : T ⟶ T
6. T ~ ℕn
7. Inj(T;T;f)
8. {x:T| (f x) = x ∈ T}  ~ ℕk
9. orbits : T List List
10. (∀o∈orbits.orbit(T;f;o))
11. ∀a:T. (∃o∈orbits. (a ∈ o))
12. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
13. no_repeats(T List;orbits)
14. n = l_sum(map(λo.||o||;orbits)) ∈ ℤ
15. (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
16. l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)}  List
⊢ ℕ||filter(λo.(||o|| =z 1);orbits)|| ~ {x:T| (f x) = x ∈ T} 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  p  :  \mBbbN{}
4.  T  :  Type
5.  f  :  T  {}\mrightarrow{}  T
6.  T  \msim{}  \mBbbN{}n
7.  Inj(T;T;f)
8.  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
9.  orbits  :  T  List  List
10.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
11.  \mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o))
12.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
13.  no\_repeats(T  List;orbits)
14.  n  =  l\_sum(map(\mlambda{}o.||o||;orbits))
15.  (\mforall{}orbit\mmember{}orbits.(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))
16.  l\_sum(map(\mlambda{}o.||o||;orbits))  \mequiv{}  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)||  mod  p
\mvdash{}  \mBbbN{}||filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)||  \msim{}  \{x:T|  (f  x)  =  x\} 


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)  \mmember{}  \{o:T  List|  (o  \mmember{}  orbits)  \mwedge{}  (||o||  =  1)\}    List\mkleeneclose{}\mcdot{}

---

Home Index