---

Step * of Lemma bsublist_functionality_wrt_bsublist

∀s:DSet. ∀as,as',bs,bs':|s| List.
  ((↑bsuplist(s;as;bs)) ⇒ (↑bsublist(s;as';bs')) ⇒ (↑(bsublist(s;as;as') ⇒b bsublist(s;bs;bs'))))
BY
{ (Auto THEN RW assert_pushdownC 0 THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index