---

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

.....assertion..... 
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. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
7. no_repeats(ℕn List;orbits)
8. ∀c1:ℕn List. ((c1 ∈ orbits) ⇒ (∀c2∈orbits.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
9. ∀c:ℕn List. ((c ∈ orbits) ⇒ (0 < ||c|| ∧ no_repeats(ℕn;c)))
10. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit) ∧ ((f a) = (cycle(orbit) a) ∈ ℕn))
11. x : ℕn
12. i : ℕ||orbits||
13. (x ∈ orbits[i])
14. (f x) = (cycle(orbits[i]) x) ∈ ℕn
⊢ ∀c:ℕn List
    ((c ∈ orbits)
    ⇒ (¬(c = orbits[i] ∈ (ℕn List)))
    ⇒ (((cycle(c) x) = x ∈ ℕn) ∧ ((cycle(c) (cycle(orbits[i]) x)) = (cycle(orbits[i]) x) ∈ ℕn)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN (Assert l_disjoint(ℕn;c;orbits[i]) BY
               OnMaybeHyp 8 (\h. (RepUR ``l_all`` h
                                  THEN (InstHyp [⌜c⌝;⌜i⌝] h⋅ THEN Auto)
                                  THEN D -1
                                  THEN Complete (Auto))))
   THEN Auto
   THEN BLemma `apply-cycle-non-member`
   THEN Auto) }

1
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. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
7. no_repeats(ℕn List;orbits)
8. ∀c1:ℕn List. ((c1 ∈ orbits) ⇒ (∀c2∈orbits.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
9. ∀c:ℕn List. ((c ∈ orbits) ⇒ (0 < ||c|| ∧ no_repeats(ℕn;c)))
10. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit) ∧ ((f a) = (cycle(orbit) a) ∈ ℕn))
11. x : ℕn
12. i : ℕ||orbits||
13. (x ∈ orbits[i])
14. (f x) = (cycle(orbits[i]) x) ∈ ℕn
15. c : ℕn List
16. (c ∈ orbits)
17. ¬(c = orbits[i] ∈ (ℕn List))
18. l_disjoint(ℕn;c;orbits[i])
⊢ ¬(x ∈ c)

2
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. (∀o1,o2∈orbits.  l_disjoint(ℕn;o1;o2))
7. no_repeats(ℕn List;orbits)
8. ∀c1:ℕn List. ((c1 ∈ orbits) ⇒ (∀c2∈orbits.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
9. ∀c:ℕn List. ((c ∈ orbits) ⇒ (0 < ||c|| ∧ no_repeats(ℕn;c)))
10. ∀a:ℕn. (∃orbit∈orbits. (a ∈ orbit) ∧ ((f a) = (cycle(orbit) a) ∈ ℕn))
11. x : ℕn
12. i : ℕ||orbits||
13. (x ∈ orbits[i])
14. (f x) = (cycle(orbits[i]) x) ∈ ℕn
15. c : ℕn List
16. (c ∈ orbits)
17. ¬(c = orbits[i] ∈ (ℕn List))
18. l_disjoint(ℕn;c;orbits[i])
19. (cycle(c) x) = x ∈ ℕn
⊢ ¬(cycle(orbits[i]) x ∈ c)

---

Latex:

---

Latex:
.....assertion..... 
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{}o1,o2\mmember{}orbits.    l\_disjoint(\mBbbN{}n;o1;o2))
7.  no\_repeats(\mBbbN{}n  List;orbits)
8.  \mforall{}c1:\mBbbN{}n  List.  ((c1  \mmember{}  orbits)  {}\mRightarrow{}  (\mforall{}c2\mmember{}orbits.(c1  =  c2)  \mvee{}  l\_disjoint(\mBbbN{}n;c1;c2)))
9.  \mforall{}c:\mBbbN{}n  List.  ((c  \mmember{}  orbits)  {}\mRightarrow{}  (0  <  ||c||  \mwedge{}  no\_repeats(\mBbbN{}n;c)))
10.  \mforall{}a:\mBbbN{}n.  (\mexists{}orbit\mmember{}orbits.  (a  \mmember{}  orbit)  \mwedge{}  ((f  a)  =  (cycle(orbit)  a)))
11.  x  :  \mBbbN{}n
12.  i  :  \mBbbN{}||orbits||
13.  (x  \mmember{}  orbits[i])
14.  (f  x)  =  (cycle(orbits[i])  x)
\mvdash{}  \mforall{}c:\mBbbN{}n  List
        ((c  \mmember{}  orbits)
        {}\mRightarrow{}  (\mneg{}(c  =  orbits[i]))
        {}\mRightarrow{}  (((cycle(c)  x)  =  x)  \mwedge{}  ((cycle(c)  (cycle(orbits[i])  x))  =  (cycle(orbits[i])  x))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (Assert  l\_disjoint(\mBbbN{}n;c;orbits[i])  BY
                          OnMaybeHyp  8  (\mbackslash{}h.  (RepUR  ``l\_all``  h
                                                                THEN  (InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THEN  Auto)
                                                                THEN  D  -1
                                                                THEN  Complete  (Auto))))
  THEN  Auto
  THEN  BLemma  `apply-cycle-non-member`
  THEN  Auto)

---

Home Index