---

Step * of Lemma lmax_com

∀s:DSet. ∀as,bs:|s| List.  (lmax(s;as;bs) ≡(|s|) lmax(s;bs;as))
BY
{ (((UnivCD THENM BLemma `permr_iff_eq_counts`) THENM D 0) THENA Auto) }

1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. x : |s|
⊢ (x #∈ lmax(s;as;bs)) = (x #∈ lmax(s;bs;as)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.    (lmax(s;as;bs)  \mequiv{}(|s|)  lmax(s;bs;as))


By

---

Latex:
(((UnivCD  THENM  BLemma  `permr\_iff\_eq\_counts`)  THENM  D  0)  THENA  Auto)

---

Home Index