---

Step * 1 1 of Lemma eqmod-by-orbits

.....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||))
⊢ l_sum(map(λo.||o||;orbits)) ≡ ||filter(λo.(||o|| =z 1);orbits)|| mod p
BY
{ (MoveToConcl (-1) THEN All Thin THEN ListInd (-1) THEN Unfold `l_sum` 0 THEN Reduce 0 THEN Try (Fold `l_sum` 0)) }

1
1. p : ℕ
2. T : Type
⊢ (∀orbit∈[].(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||)) ⇒ (0 ≡ 0 mod p)

2
1. p : ℕ
2. T : Type
3. u : T List
4. v : T List List
5. (∀orbit∈v.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||)) ⇒ (l_sum(map(λo.||o||;v)) ≡ ||filter(λo.(||o|| =z 1);v)|| mod p)
⊢ (∀orbit∈[u / v].(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||))
⇒ ((||u|| + l_sum(map(λo.||o||;v))) ≡ ||if (||u|| =z 1)
   then [u / filter(λo.(||o|| =z 1);v)]
   else filter(λo.(||o|| =z 1);v)
   fi || mod p)

---

Latex:

---

Latex:
.....assertion..... 
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||))
\mvdash{}  l\_sum(map(\mlambda{}o.||o||;orbits))  \mequiv{}  ||filter(\mlambda{}o.(||o||  =\msubz{}  1);orbits)||  mod  p


By

---

Latex:
(MoveToConcl  (-1)
  THEN  All  Thin
  THEN  ListInd  (-1)
  THEN  Unfold  `l\_sum`  0
  THEN  Reduce  0
  THEN  Try  (Fold  `l\_sum`  0))

---

Home Index