---

Step * of Lemma parallel-bag-classrel

∀[B,Info,T:Type]. ∀[X:T ⟶ EClass(B)]. ∀[as:bag(T)]. ∀[v:B]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(v ∈ (||a∈as.X[a])(e);↓∃a:T. (a ↓∈ as ∧ v ∈ X[a](e)))
BY
{ (Intros⋅
   THEN Unfold `parallel-bag-class` 0
   THEN ((RWO "bind-class-rel" 0 THENA Auto)
         THEN (RWO "return-loc-bag-class-classrel" 0 THENA Auto)
         THEN Reduce 0
         THEN Auto)) }

1
1. B : Type
2. Info : Type
3. T : Type
4. X : T ⟶ EClass(B)
5. as : bag(T)
6. v : B
7. es : EO+(Info)
8. e : E
9. ∃a:T. (a ↓∈ as ∧ v ∈ X[a](e))
⊢ ↓∃e':{e':E| e' ≤loc e } . ∃a:T. ((a ↓∈ as ∧ (↑first(e'))) ∧ v ∈ X[a](e))

---

Latex:

---

Latex:
\mforall{}[B,Info,T:Type].  \mforall{}[X:T  {}\mrightarrow{}  EClass(B)].  \mforall{}[as:bag(T)].  \mforall{}[v:B].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(v  \mmember{}  (||a\mmember{}as.X[a])(e);\mdownarrow{}\mexists{}a:T.  (a  \mdownarrow{}\mmember{}  as  \mwedge{}  v  \mmember{}  X[a](e)))


By

---

Latex:
(Intros\mcdot{}
  THEN  Unfold  `parallel-bag-class`  0
  THEN  ((RWO  "bind-class-rel"  0  THENA  Auto)
              THEN  (RWO  "return-loc-bag-class-classrel"  0  THENA  Auto)
              THEN  Reduce  0
              THEN  Auto))

---

Home Index