---

Step * of Lemma bag-extensionality2

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].
  uiff(as = bs ∈ bag(T);(∀x:T. (x ↓∈ as ⇒ ((#x in as) = (#x in bs) ∈ ℤ))) ∧ (∀x:T. (x ↓∈ bs ⇒ x ↓∈ as)))
BY
{ (InstLemma `bag-extensionality` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN Decide 0 < (#x in as)
   THEN Auto
   THEN Decide 0 < (#x in bs)
   THEN Auto
   THEN Auto'
   THEN BackThruSomeHyp
   THEN (InstLemma `bag-member-count` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)⋅
   THEN Try ((BHyp -1  THEN Complete (Auto)))
   THEN OnMaybeHyp 6 (\h. (BHyp h THEN Auto THEN (BHyp -1  THEN Complete (Auto))⋅))) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].
    uiff(as  =  bs;(\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  ((\#x  in  as)  =  (\#x  in  bs))))  \mwedge{}  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  as)))


By

---

Latex:
(InstLemma  `bag-extensionality`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  Decide  0  <  (\#x  in  as)
  THEN  Auto
  THEN  Decide  0  <  (\#x  in  bs)
  THEN  Auto
  THEN  Auto'
  THEN  BackThruSomeHyp
  THEN  (InstLemma  `bag-member-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  Try  ((BHyp  -1    THEN  Complete  (Auto)))
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (BHyp  h  THEN  Auto  THEN  (BHyp  -1    THEN  Complete  (Auto))\mcdot{})))

---

Home Index