---

Step * of Lemma classrel-at

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[locs:bag(Id)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  (v ∈ X@locs(e) ⇐⇒ loc(e) ↓∈ locs ∧ v ∈ X(e))
BY
{ ((Auto THEN All (Unfold `classrel`))
   THEN Try ((RepUR ``class-at`` (-1)
              THEN (SplitOnHypITE -1  THENA Auto)
              THEN Try ((FLemma `bag-member-empty` [-2] THEN Auto))
              THEN Auto))
   THEN Try ((RepUR ``class-at`` 0 THEN SplitOnConclITE THEN Auto)⋅)) }

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[locs:bag(Id)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    (v  \mmember{}  X@locs(e)  \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs  \mwedge{}  v  \mmember{}  X(e))


By

---

Latex:
((Auto  THEN  All  (Unfold  `classrel`))
  THEN  Try  ((RepUR  ``class-at``  (-1)
                        THEN  (SplitOnHypITE  -1    THENA  Auto)
                        THEN  Try  ((FLemma  `bag-member-empty`  [-2]  THEN  Auto))
                        THEN  Auto))
  THEN  Try  ((RepUR  ``class-at``  0  THEN  SplitOnConclITE  THEN  Auto)\mcdot{}))

---

Home Index