---

Step * 1 2 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)
19. no_repeats(T;concat(orbits))
20. ||concat(orbits)|| = ||concat(orbits)|| ∈ ℤ
21. x : T
⊢ (x ∈ concat(orbits))
BY
{ (BLemma `member-concat` THEN Auto THEN BLemma `l_exists_iff` THEN Auto THEN BackThruSomeHyp⋅) }

---

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)
19.  no\_repeats(T;concat(orbits))
20.  ||concat(orbits)||  =  ||concat(orbits)||
21.  x  :  T
\mvdash{}  (x  \mmember{}  concat(orbits))


By

---

Latex:
(BLemma  `member-concat`  THEN  Auto  THEN  BLemma  `l\_exists\_iff`  THEN  Auto  THEN  BackThruSomeHyp\mcdot{})

---

Home Index