---

Step * 1 2 1 2 2 3 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
17. filter(λo.(||o|| =z 1);orbits) ∈ {o:T List| (o ∈ orbits) ∧ (||o|| = 1 ∈ ℤ)}  List
18. b : {x:T| (f x) = x ∈ T} 
⊢ ∃a:ℕ||filter(λo.(||o|| =z 1);orbits)||. (hd(filter(λo.(||o|| =z 1);orbits)[a]) = b ∈ {x:T| (f x) = x ∈ T} )
BY
{ TACTIC:((Assert (∃orbit∈orbits. (b ∈ orbit)) BY Auto) THEN (RWO "l_exists_iff" (-1) THENA Auto) THEN D -1) }

1
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
18. b : {x:T| (f x) = x ∈ T} 
19. orbit : T List
20. (orbit ∈ orbits) ∧ (b ∈ orbit)
⊢ ∃a:ℕ||filter(λo.(||o|| =z 1);orbits)||. (hd(filter(λo.(||o|| =z 1);orbits)[a]) = b ∈ {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
17.  filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)  \mmember{}  \{o:T  List|  (o  \mmember{}  orbits)  \mwedge{}  (||o||  =  1)\}    List
18.  b  :  \{x:T|  (f  x)  =  x\} 
\mvdash{}  \mexists{}a:\mBbbN{}||filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)||.  (hd(filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)[a])  =  b)


By

---

Latex:
TACTIC:((Assert  (\mexists{}orbit\mmember{}orbits.  (b  \mmember{}  orbit))  BY
                              Auto)
                THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
                THEN  D  -1)

---

Home Index