---

Step * 1 1 of Lemma bsubmset_functionality_wrt_bsubmset


1. s : DSet
⊢ ∀a,a',b,b':|s| List.
    ((↑(mk_mset(b) ⊆b mk_mset(a)))
    ⇒ (↑(mk_mset(a') ⊆b mk_mset(b')))
    ⇒ (↑(mk_mset(a) ⊆b mk_mset(a') ⇒b (mk_mset(b) ⊆b mk_mset(b')))))
BY
{ ((RepD  
THENM RW bool_to_propC 0 
THENM D 0 
THENM All (RWW "bsubmset_elim") 
THENM RelRST) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
\mvdash{}  \mforall{}a,a',b,b':|s|  List.
        ((\muparrow{}(mk\_mset(b)  \msubseteq{}\msubb{}  mk\_mset(a)))
        {}\mRightarrow{}  (\muparrow{}(mk\_mset(a')  \msubseteq{}\msubb{}  mk\_mset(b')))
        {}\mRightarrow{}  (\muparrow{}(mk\_mset(a)  \msubseteq{}\msubb{}  mk\_mset(a')  {}\mRightarrow{}\msubb{}  (mk\_mset(b)  \msubseteq{}\msubb{}  mk\_mset(b')))))


By

---

Latex:
((RepD   
THENM  RW  bool\_to\_propC  0 
THENM  D  0 
THENM  All  (RWW  "bsubmset\_elim") 
THENM  RelRST)  THEN  Auto)

---

Home Index