Step
*
1
2
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
⊢ l_sum(map(λo.||o||;orbits)) ≡ k mod p
BY
{ TACTIC:((RWO "-1" 0 THEN Auto)
          THEN BLemma `eqmod_weakening`
          THEN Auto
          THEN (BLemma `equipollent-nsub` THENA Auto)
          THEN (RWO "8<" 0 THENA Auto)) }
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
⊢ ℕ||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{}  l\_sum(map(\mlambda{}o.||o||;orbits))  \mequiv{}  k  mod  p
By
Latex:
TACTIC:((RWO  "-1"  0  THEN  Auto)
                THEN  BLemma  `eqmod\_weakening`
                THEN  Auto
                THEN  (BLemma  `equipollent-nsub`  THENA  Auto)
                THEN  (RWO  "8<"  0  THENA  Auto))
Home
Index