---

Step * of Lemma bsublist_functionality_wrt_permr

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

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

---

Latex:

---

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


By

---

Latex:
(RepD  THENA  Auto)

---

Home Index