---

Step * 2 1 2 of Lemma combinations-list


1. A : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
5. c : ℕ
6. Combination(k;A) ~ ℕc
7. L : Combination(k;A) List
8. no_repeats(Combination(k;A);L)
9. ||L|| = c ∈ ℤ
10. ∀x:Combination(k;A). (x ∈ L)
11. L@0 : A List
12. (L@0 ∈ L)
⊢ no_repeats(A;L@0)
BY
{ xxx(RepeatFor 2 (D -1) THEN HypSubst' (-1) 0 THEN Auto THEN (GenConclAtAddr [2] THEN D -2) THEN Auto)xxx }

1
1. A : Type
2. n : ℕ
3. A ~ ℕn
4. k : ℕ
5. c : ℕ
6. Combination(k;A) ~ ℕc
7. L : Combination(k;A) List
8. no_repeats(Combination(k;A);L)
9. ||L|| = c ∈ ℤ
10. ∀x:Combination(k;A). (x ∈ L)
11. L@0 : A List
12. i : ℕ
13. i < ||L||
14. L@0 = L[i] ∈ (A List)
15. v : A List
16. [%22] : no_repeats(A;v) ∧ (||v|| = k ∈ ℤ)
17. L[i] = v ∈ Combination(k;A)
⊢ no_repeats(A;v)

---

Latex:

---

Latex:

1.  A  :  Type
2.  n  :  \mBbbN{}
3.  A  \msim{}  \mBbbN{}n
4.  k  :  \mBbbN{}
5.  c  :  \mBbbN{}
6.  Combination(k;A)  \msim{}  \mBbbN{}c
7.  L  :  Combination(k;A)  List
8.  no\_repeats(Combination(k;A);L)
9.  ||L||  =  c
10.  \mforall{}x:Combination(k;A).  (x  \mmember{}  L)
11.  L@0  :  A  List
12.  (L@0  \mmember{}  L)
\mvdash{}  no\_repeats(A;L@0)


By

---

Latex:
xxx(RepeatFor  2  (D  -1)
        THEN  HypSubst'  (-1)  0
        THEN  Auto
        THEN  (GenConclAtAddr  [2]  THEN  D  -2)
        THEN  Auto)xxx

---

Home Index