---

Step * 1 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)
⊢ no_repeats(T;concat(orbits))
BY
{ (BLemma `no_repeats-concat` THEN Auto THEN RepeatFor 2 (ParallelOp 11) THEN Auto) }

---

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{}  no\_repeats(T;concat(orbits))


By

---

Latex:
(BLemma  `no\_repeats-concat`  THEN  Auto  THEN  RepeatFor  2  (ParallelOp  11)  THEN  Auto)

---

Home Index