---

Step * of Lemma distinct_iff_counts_le_one

∀s:DSet. ∀ps:|s| List.  (↑distinct{s}(ps) ⇐⇒ ∀x:|s|. ((x #∈ ps) ≤ 1))
BY
{ TACTIC:(InductionOnListA THEN Reduce 0) }

1
1. s : DSet
⊢ True ⇐⇒ ∀x:|s|. (0 ≤ 1)

2
1. s : DSet
2. p : |s|
3. ps : |s| List
4. ↑distinct{s}(ps) ⇐⇒ ∀x:|s|. ((x #∈ ps) ≤ 1)
⊢ ↑((∀br(:|s|) ∈ ps. (¬b(r (=b) p))) ∧b distinct{s}(ps)) ⇐⇒ ∀x:|s|. ((b2i(p (=b) x) + (x #∈ ps)) ≤ 1)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}ps:|s|  List.    (\muparrow{}distinct\{s\}(ps)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((x  \#\mmember{}  ps)  \mleq{}  1))


By

---

Latex:
TACTIC:(InductionOnListA  THEN  Reduce  0)

---

Home Index