---

Step * of Lemma count-by-orbits

∀n:ℕ
  ∀[T:Type]
    (T ~ ℕn
    ⇒ (∀f:T ⟶ T
          ∃orbits:T List List
           ((∀o∈orbits.orbit(T;f;o))
           ∧ (∀a:T. (∃o∈orbits. (a ∈ o)))
           ∧ (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
           ∧ no_repeats(T List;orbits)
           ∧ (n = l_sum(map(λo.||o||;orbits)) ∈ ℤ)) 
          supposing Inj(T;T;f)))
BY
{ (Auto
   THEN (FLemma `equipollent_inversion` [-3] THENA Auto)
   THEN RepeatFor 2 (D -4)
   THEN (RenameVar `h' 3
         THEN (Assert ∀x,y:T.  Dec(x = y ∈ T) BY
                     (Auto THEN (Assert ⌜Dec((h x) = (h y) ∈ ℤ)⌝⋅ THEN Auto) THEN Repeat (ParallelLast) THEN Auto'))
         )
   THEN (InstLemma `orbit-decomp2` [⌜T⌝;⌜f⌝]⋅ THENA (Auto THEN RepeatFor 2 (D -2) THEN With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN Try ((ExRepD THEN InstConcl [⌜orbits⌝]⋅ THEN Auto))) }

1
1. n : ℕ
2. T : Type
3. h : T ⟶ ℕn
4. Inj(T;ℕn;h)
5. Surj(T;ℕn;h)
6. f : T ⟶ T
7. Inj(T;T;f)
8. ℕn ~ T
9. ∀x,y:T.  Dec(x = y ∈ T)
10. orbits : T List List
11. (∀o∈orbits.orbit(T;f;o))
12. ∀a:T. (∃orbit∈orbits. (a ∈ orbit))
13. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
14. no_repeats(T List;orbits)
15. (∀o∈orbits.orbit(T;f;o))
16. ∀a:T. (∃o∈orbits. (a ∈ o))
17. (∀o1,o2∈orbits.  l_disjoint(T;o1;o2))
18. no_repeats(T List;orbits)
⊢ n = l_sum(map(λo.||o||;orbits)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mforall{}[T:Type]
        (T  \msim{}  \mBbbN{}n
        {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T
                    \mexists{}orbits:T  List  List
                      ((\mforall{}o\mmember{}orbits.orbit(T;f;o))
                      \mwedge{}  (\mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o)))
                      \mwedge{}  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
                      \mwedge{}  no\_repeats(T  List;orbits)
                      \mwedge{}  (n  =  l\_sum(map(\mlambda{}o.||o||;orbits)))) 
                    supposing  Inj(T;T;f)))


By

---

Latex:
(Auto
  THEN  (FLemma  `equipollent\_inversion`  [-3]  THENA  Auto)
  THEN  RepeatFor  2  (D  -4)
  THEN  (RenameVar  `h'  3
              THEN  (Assert  \mforall{}x,y:T.    Dec(x  =  y)  BY
                                      (Auto
                                        THEN  (Assert  \mkleeneopen{}Dec((h  x)  =  (h  y))\mkleeneclose{}\mcdot{}  THEN  Auto)
                                        THEN  Repeat  (ParallelLast)
                                        THEN  Auto'))
              )
  THEN  (InstLemma  `orbit-decomp2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepeatFor  2  (D  -2)  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
              )
  THEN  Try  ((ExRepD  THEN  InstConcl  [\mkleeneopen{}orbits\mkleeneclose{}]\mcdot{}  THEN  Auto)))

---

Home Index