---

Step * of Lemma return-loc-bag-class-classrel

∀[Info,A:Type]. ∀[x:Id ⟶ bag(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
  (v ∈ return-loc-bag-class(x)(e) ⇐⇒ v ↓∈ x loc(e) ∧ (↑first(e)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``return-loc-bag-class classrel`` 0 THEN AutoSplit THEN Auto THEN BagMemberD (-1)) }

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[x:Id  {}\mrightarrow{}  bag(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:A].
    (v  \mmember{}  return-loc-bag-class(x)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mdownarrow{}\mmember{}  x  loc(e)  \mwedge{}  (\muparrow{}first(e)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``return-loc-bag-class  classrel``  0
  THEN  AutoSplit
  THEN  Auto
  THEN  BagMemberD  (-1))

---

Home Index