---

Step * of Lemma eqmod-by-orbits

No Annotations
∀n,k,p:ℕ.
  ((∃T:Type
     ∃f:T ⟶ T
      (T ~ ℕn
      ∧ Inj(T;T;f)
      ∧ {x:T| (f x) = x ∈ T}  ~ ℕk
      ∧ (∀L:T List. (||L|| = 1 ∈ ℤ) ∨ (p | ||L||) supposing orbit(T;f;L))))
  ⇒ (n ≡ k mod p))
BY
{ (Auto
   THEN ExRepD
   THEN (InstLemma `count-by-orbits` [⌜n⌝;⌜T⌝;⌜f⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN HypSubst' -1 0
   THEN ((Assert (∀orbit∈orbits.(||orbit|| = 1 ∈ ℤ) ∨ (p | ||orbit||)) BY
                ((D 0 THENA Auto) THEN BackThruSomeHyp THEN BackThruSomeHyp'))
         THEN Thin (-8)
         )⋅) }

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||))
⊢ l_sum(map(λo.||o||;orbits)) ≡ k mod p

---

Latex:

---

Latex:
No  Annotations
\mforall{}n,k,p:\mBbbN{}.
    ((\mexists{}T:Type
          \mexists{}f:T  {}\mrightarrow{}  T
            (T  \msim{}  \mBbbN{}n
            \mwedge{}  Inj(T;T;f)
            \mwedge{}  \{x:T|  (f  x)  =  x\}    \msim{}  \mBbbN{}k
            \mwedge{}  (\mforall{}L:T  List.  (||L||  =  1)  \mvee{}  (p  |  ||L||)  supposing  orbit(T;f;L))))
    {}\mRightarrow{}  (n  \mequiv{}  k  mod  p))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstLemma  `count-by-orbits`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  HypSubst'  -1  0
  THEN  ((Assert  (\mforall{}orbit\mmember{}orbits.(||orbit||  =  1)  \mvee{}  (p  |  ||orbit||))  BY
                            ((D  0  THENA  Auto)  THEN  BackThruSomeHyp  THEN  BackThruSomeHyp'))
              THEN  Thin  (-8)
              )\mcdot{})

---

Home Index