---

Step * of Lemma combination-decomp

∀[A:Type]. ∀[n:ℕ+]. ∀[L:Combination(n;A)].  {(hd(L) ∈ A) ∧ (tl(L) ∈ Combination(n - 1;{a:A| ¬(a = hd(L) ∈ A)} ))}
BY
{ xxx(Auto THEN D -1 THEN D -2 THEN Reduce 0 THEN Unfold `guard` 0 THEN D 0 THEN Unhide THEN All Reduce THEN Auto')xxx }

1
1. A : Type
2. n : ℕ+
3. u : A
4. v : A List
5. no_repeats(A;[u / v])
6. (||v|| + 1) = n ∈ ℤ
⊢ v ∈ Combination(n - 1;{a:A| ¬(a = u ∈ A)} )

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[L:Combination(n;A)].
    \{(hd(L)  \mmember{}  A)  \mwedge{}  (tl(L)  \mmember{}  Combination(n  -  1;\{a:A|  \mneg{}(a  =  hd(L))\}  ))\}


By

---

Latex:
xxx(Auto
        THEN  D  -1
        THEN  D  -2
        THEN  Reduce  0
        THEN  Unfold  `guard`  0
        THEN  D  0
        THEN  Unhide
        THEN  All  Reduce
        THEN  Auto')xxx

---

Home Index