---

Step * of Lemma bsublist_append_diff

∀s:DSet. ∀as,bs:|s| List.  ((↑bsublist(s;as;bs)) ⇒ (∃cs:|s| List. ((cs @ as) ≡(|s|) bs)))
BY
{ ((RepD THENM With bs - as (D 0)) THENA Auto) }

1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. ↑bsublist(s;as;bs)
⊢ ((bs - as) @ as) ≡(|s|) bs

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.    ((\muparrow{}bsublist(s;as;bs))  {}\mRightarrow{}  (\mexists{}cs:|s|  List.  ((cs  @  as)  \mequiv{}(|s|)  bs)))


By

---

Latex:
((RepD  THENM  With  bs  -  as  (D  0))  THENA  Auto)

---

Home Index