---

Step * 2 1 1 2 2 1 1 1 of Lemma cyclic-map-equipollent


1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. a1 : ℕn - 1 List
4. no_repeats(ℕn - 1;a1)
5. ||a1|| = (n - 1) ∈ ℤ
6. a2 : ℕn - 1 List
7. no_repeats(ℕn - 1;a2)
8. ||a2|| = (n - 1) ∈ ℤ
9. cycle([n - 1 / a1]) = cycle([n - 1 / a2]) ∈ ℕn →⟶ ℕn
10. ∀x,y:ℕn.  ∃n@0:ℕ. ((cycle([n - 1 / a1])^n@0 x) = y ∈ ℕn)
11. i : ℕ
12. i < ||a1||
13. (cycle([n - 1 / a1])^(i + 1) - 0 (n - 1)) = a1[(i + 1) - 1] ∈ ℕn
14. (cycle([n - 1 / a2])^(i + 1) - 0 (n - 1)) = a2[(i + 1) - 1] ∈ ℕn
⊢ (cycle([n - 1 / a1])^(i + 1) - 0 (n - 1)) = (cycle([n - 1 / a2])^(i + 1) - 0 (n - 1)) ∈ ℕn
BY
{ xxx(EqTypeHD (-6)
      THENA (Auto
             THEN DVar `f'
             THEN xxx(Try ((GenConclAtAddr [2] THEN Complete (Auto)))
                      THEN Try ((GenConclAtAddr [1] THEN Complete (Auto)))
                      )xxx)
      )xxx }

1
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. a1 : ℕn - 1 List
4. no_repeats(ℕn - 1;a1)
5. ||a1|| = (n - 1) ∈ ℤ
6. a2 : ℕn - 1 List
7. no_repeats(ℕn - 1;a2)
8. ||a2|| = (n - 1) ∈ ℤ
9. cycle([n - 1 / a1]) = cycle([n - 1 / a2]) ∈ (ℕn ⟶ ℕn)
10. Inj(ℕn;ℕn;cycle([n - 1 / a1]))
11. ∀x,y:ℕn.  ∃n@0:ℕ. ((cycle([n - 1 / a1])^n@0 x) = y ∈ ℕn)
12. i : ℕ
13. i < ||a1||
14. (cycle([n - 1 / a1])^(i + 1) - 0 (n - 1)) = a1[(i + 1) - 1] ∈ ℕn
15. (cycle([n - 1 / a2])^(i + 1) - 0 (n - 1)) = a2[(i + 1) - 1] ∈ ℕn
⊢ (cycle([n - 1 / a1])^(i + 1) - 0 (n - 1)) = (cycle([n - 1 / a2])^(i + 1) - 0 (n - 1)) ∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  \mforall{}L:Combination(n  -  1;\mBbbN{}n  -  1).  ([n  -  1  /  L]  \mmember{}  Combination(n;\mBbbN{}n))
3.  a1  :  \mBbbN{}n  -  1  List
4.  no\_repeats(\mBbbN{}n  -  1;a1)
5.  ||a1||  =  (n  -  1)
6.  a2  :  \mBbbN{}n  -  1  List
7.  no\_repeats(\mBbbN{}n  -  1;a2)
8.  ||a2||  =  (n  -  1)
9.  cycle([n  -  1  /  a1])  =  cycle([n  -  1  /  a2])
10.  \mforall{}x,y:\mBbbN{}n.    \mexists{}n@0:\mBbbN{}.  ((cycle([n  -  1  /  a1])\^{}n@0  x)  =  y)
11.  i  :  \mBbbN{}
12.  i  <  ||a1||
13.  (cycle([n  -  1  /  a1])\^{}(i  +  1)  -  0  (n  -  1))  =  a1[(i  +  1)  -  1]
14.  (cycle([n  -  1  /  a2])\^{}(i  +  1)  -  0  (n  -  1))  =  a2[(i  +  1)  -  1]
\mvdash{}  (cycle([n  -  1  /  a1])\^{}(i  +  1)  -  0  (n  -  1))  =  (cycle([n  -  1  /  a2])\^{}(i  +  1)  -  0  (n  -  1))


By

---

Latex:
xxx(EqTypeHD  (-6)
        THENA  (Auto
                      THEN  DVar  `f'
                      THEN  xxx(Try  ((GenConclAtAddr  [2]  THEN  Complete  (Auto)))
                                        THEN  Try  ((GenConclAtAddr  [1]  THEN  Complete  (Auto)))
                                        )xxx)
        )xxx

---

Home Index