---

Step * of Lemma send-once-loc-classrel

∀[Info,A:Type]. ∀[b:Id ─→ bag(A)].
  ∀es:EO+(Info). ∀e:E. ∀v:A.  (v ∈ send-once-loc-class(b)(e) ⇐⇒ v ↓∈ b loc(e) ∧ (↑first(e)))
BY
{ (((UnivCD THENA Auto)
    THEN Unfold `send-once-loc-class` 0
    THEN (RWO "once-classrel" 0 THENA (Auto THEN Try ((Unfold `eclass` 0 THEN Auto)))))
   THEN RepUR ``classrel`` 0
   THEN Auto
   THEN Try ((D 0 THEN Auto))) }

1
1. Info : Type
2. A : Type
3. b : Id ─→ bag(A)
4. es : EO+(Info)@i'
5. e : E@i
6. v : A@i
7. (no λes,e. (b loc(e)) prior to e)@i
8. v ↓∈ b loc(e)@i
⊢ ↑first(e)

---

Latex:

---

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


By

---

Latex:
(((UnivCD  THENA  Auto)
    THEN  Unfold  `send-once-loc-class`  0
    THEN  (RWO  "once-classrel"  0  THENA  (Auto  THEN  Try  ((Unfold  `eclass`  0  THEN  Auto)))))
  THEN  RepUR  ``classrel``  0
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto)))

---

Home Index