---

Step * of Lemma lmax_functionality_wrt_permr

∀s:DSet. ∀as,as',bs,bs':|s| List.  ((as ≡(|s|) as') ⇒ (bs ≡(|s|) bs') ⇒ (lmax(s;as;bs) ≡(|s|) lmax(s;as';bs')))
BY
{ Auto }

1
1. s : DSet
2. as : |s| List
3. as' : |s| List
4. bs : |s| List
5. bs' : |s| List
6. as ≡(|s|) as'
7. bs ≡(|s|) bs'
⊢ lmax(s;as;bs) ≡(|s|) lmax(s;as';bs')

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index