---

Step * of Lemma cycle-conjugate

∀[n:ℕ]. ∀[L:ℕn List].
  ∀[f,g:ℕn ⟶ ℕn].
    ((g o (cycle(L) o f)) = cycle(map(g;L)) ∈ (ℕn ⟶ ℕn)) supposing 
       ((∀a:ℕn. ((f (g a)) = a ∈ ℕn)) and 
       (∀a:ℕn. ((g (f a)) = a ∈ ℕn))) 
  supposing no_repeats(ℕn;L)
BY
{ TACTIC:(Auto THEN Ext THEN Reduce 0 THEN Auto) }

1
1. n : ℕ
2. L : ℕn List
3. no_repeats(ℕn;L)
4. f : ℕn ⟶ ℕn
5. g : ℕn ⟶ ℕn
6. ∀a:ℕn. ((g (f a)) = a ∈ ℕn)
7. ∀a:ℕn. ((f (g a)) = a ∈ ℕn)
8. x : ℕn
⊢ (g (cycle(L) (f x))) = (cycle(map(g;L)) x) ∈ ℕn

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:\mBbbN{}n  List].
    \mforall{}[f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n].
        ((g  o  (cycle(L)  o  f))  =  cycle(map(g;L)))  supposing 
              ((\mforall{}a:\mBbbN{}n.  ((f  (g  a))  =  a))  and 
              (\mforall{}a:\mBbbN{}n.  ((g  (f  a))  =  a))) 
    supposing  no\_repeats(\mBbbN{}n;L)


By

---

Latex:
TACTIC:(Auto  THEN  Ext  THEN  Reduce  0  THEN  Auto)

---

Home Index