---

Step * of Lemma single-valued-sub-bag

∀[T:Type]. ∀[as,bs:bag(T)].  (single-valued-bag(bs;T) ⇒ sub-bag(T;as;bs) ⇒ single-valued-bag(as;T))
BY
{ (Auto
   THEN (InstLemma `sub-bag-member` [⌜T⌝;⌜as⌝;⌜bs⌝]⋅ THEN Auto)
   THEN RepeatFor 2 (ParallelOp -3)
   THEN RepeatFor 3 ((ParallelLast THENA Auto))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].
    (single-valued-bag(bs;T)  {}\mRightarrow{}  sub-bag(T;as;bs)  {}\mRightarrow{}  single-valued-bag(as;T))


By

---

Latex:
(Auto
  THEN  (InstLemma  `sub-bag-member`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  RepeatFor  2  (ParallelOp  -3)
  THEN  RepeatFor  3  ((ParallelLast  THENA  Auto)))

---

Home Index