---

Step * 1 of Lemma count-by-orbits


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)) ∈ ℤ
BY
{ ((RWO "length-concat<" 0
    THENM BLemma `equipollent-nsub`
    THENM RWO "8" 0
    THENM BLemma `equipollent-iff-list` 
    THENM InstConcl [⌜concat(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)
⊢ no_repeats(T;concat(orbits))

2
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)
19. no_repeats(T;concat(orbits))
20. ||concat(orbits)|| = ||concat(orbits)|| ∈ ℤ
21. x : T
⊢ (x ∈ concat(orbits))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  T  :  Type
3.  h  :  T  {}\mrightarrow{}  \mBbbN{}n
4.  Inj(T;\mBbbN{}n;h)
5.  Surj(T;\mBbbN{}n;h)
6.  f  :  T  {}\mrightarrow{}  T
7.  Inj(T;T;f)
8.  \mBbbN{}n  \msim{}  T
9.  \mforall{}x,y:T.    Dec(x  =  y)
10.  orbits  :  T  List  List
11.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
12.  \mforall{}a:T.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
13.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
14.  no\_repeats(T  List;orbits)
15.  (\mforall{}o\mmember{}orbits.orbit(T;f;o))
16.  \mforall{}a:T.  (\mexists{}o\mmember{}orbits.  (a  \mmember{}  o))
17.  (\mforall{}o1,o2\mmember{}orbits.    l\_disjoint(T;o1;o2))
18.  no\_repeats(T  List;orbits)
\mvdash{}  n  =  l\_sum(map(\mlambda{}o.||o||;orbits))


By

---

Latex:
((RWO  "length-concat<"  0
    THENM  BLemma  `equipollent-nsub`
    THENM  RWO  "8"  0
    THENM  BLemma  `equipollent-iff-list` 
    THENM  InstConcl  [\mkleeneopen{}concat(orbits)\mkleeneclose{}]\mcdot{})
  THEN  Auto
  )

---

Home Index