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 0) THENA Auto) }

1
1. DSet
2. as |s| List
3. bs |s| List
4. |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