---

Step * of Lemma lmax_assoc

∀s:DSet. ∀as,bs,cs:|s| List.  (lmax(s;as;lmax(s;bs;cs)) ≡(|s|) lmax(s;lmax(s;as;bs);cs))
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. cs : |s| List
5. x : |s|
⊢ (x #∈ lmax(s;as;lmax(s;bs;cs))) = (x #∈ lmax(s;lmax(s;as;bs);cs)) ∈ ℤ

---

Latex:

---

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


By

---

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

---

Home Index