---

Step * 2 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]) ∈ cyclic-map(ℕn)
10. i : ℕ
11. i < ||a1||
⊢ a1[i] = a2[i] ∈ ℕn - 1
BY
{ xxx((InstLemma `cycle-transitive1` [⌜n⌝;⌜[n - 1 / a1]⌝;⌜0⌝;⌜i + 1⌝]⋅ THENA (Reduce 0 THEN Auto))
      THEN Reduce (-1)
      )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]) ∈ cyclic-map(ℕn)
10. i : ℕ
11. i < ||a1||
12. no_repeats(ℕn;a1)
⊢ ¬(n - 1 ∈ a1)

2
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]) ∈ cyclic-map(ℕn)
10. i : ℕ
11. i < ||a1||
12. (cycle([n - 1 / a1])^(i + 1) - 0 (n - 1)) = [n - 1 / a1][i + 1] ∈ ℕn
⊢ a1[i] = a2[i] ∈ ℕn - 1

---

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.  i  :  \mBbbN{}
11.  i  <  ||a1||
\mvdash{}  a1[i]  =  a2[i]


By

---

Latex:
xxx((InstLemma  `cycle-transitive1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}[n  -  1  /  a1]\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}i  +  1\mkleeneclose{}]\mcdot{}  THENA  (Reduce  0  THEN  Auto))
        THEN  Reduce  (-1)
        )xxx

---

Home Index