---

Step * 1 1 2 1 1 of Lemma cycle-decomp


1. n : ℕ
2. f : {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} 
3. orbits : ℕn List List
4. ∀orbit:ℕn List
     ((orbit ∈ orbits)
     ⇒ (0 < ||orbit||
        ∧ no_repeats(ℕn;orbit)
        ∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi  ∈ ℕn))
        ∧ (∀x∈orbit.∀n@0:ℕ. (f^n@0 x ∈ orbit))))
5. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit))
6. ∀i:ℕ||orbits||. ∀j:ℕi.  l_disjoint(ℕn;orbits[j];orbits[i])
7. i : ℕ
8. j : ℕ
9. i < ||orbits||
10. j < ||orbits||
11. orbits[i] = orbits[j] ∈ (ℕn List)
12. ¬i < j
13. j < i
14. l_disjoint(ℕn;orbits[j];orbits[j])
⊢ i = j ∈ ℕ
BY
{ ((Assert 0 < ||orbits[j]|| BY
          Auto)
   THEN Unfold `l_disjoint` (-2)
   THEN (InstHyp [⌜orbits[j][0]⌝] (-2)⋅ THENM D -1)
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  f  :  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;f)\} 
3.  orbits  :  \mBbbN{}n  List  List
4.  \mforall{}orbit:\mBbbN{}n  List
          ((orbit  \mmember{}  orbits)
          {}\mRightarrow{}  (0  <  ||orbit||
                \mwedge{}  no\_repeats(\mBbbN{}n;orbit)
                \mwedge{}  (\mforall{}i:\mBbbN{}||orbit||
                          ((f  orbit[i])  =  if  (i  =\msubz{}  ||orbit||  -  1)  then  orbit[0]  else  orbit[i  +  1]  fi  ))
                \mwedge{}  (\mforall{}x\mmember{}orbit.\mforall{}n@0:\mBbbN{}.  (f\^{}n@0  x  \mmember{}  orbit))))
5.  \mforall{}a:\mBbbN{}n.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit))
6.  \mforall{}i:\mBbbN{}||orbits||.  \mforall{}j:\mBbbN{}i.    l\_disjoint(\mBbbN{}n;orbits[j];orbits[i])
7.  i  :  \mBbbN{}
8.  j  :  \mBbbN{}
9.  i  <  ||orbits||
10.  j  <  ||orbits||
11.  orbits[i]  =  orbits[j]
12.  \mneg{}i  <  j
13.  j  <  i
14.  l\_disjoint(\mBbbN{}n;orbits[j];orbits[j])
\mvdash{}  i  =  j


By

---

Latex:
((Assert  0  <  ||orbits[j]||  BY
                Auto)
  THEN  Unfold  `l\_disjoint`  (-2)
  THEN  (InstHyp  [\mkleeneopen{}orbits[j][0]\mkleeneclose{}]  (-2)\mcdot{}  THENM  D  -1)
  THEN  Auto)\mcdot{}

---

Home Index