---

Step * 1 of Lemma bsubmset_wf


1. s : DSet
2. as : |s| List
3. bs : |s| List
4. as ≡(|s|) bs
5. v : |s| List
6. v1 : |s| List
7. v ≡(|s|) v1
⊢ bsublist(s;as;v) = bsublist(s;bs;v1)
BY
{ (RWW "4 7" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  |s|  List
3.  bs  :  |s|  List
4.  as  \mequiv{}(|s|)  bs
5.  v  :  |s|  List
6.  v1  :  |s|  List
7.  v  \mequiv{}(|s|)  v1
\mvdash{}  bsublist(s;as;v)  =  bsublist(s;bs;v1)


By

---

Latex:
(RWW  "4  7"  0  THEN  Auto)

---

Home Index