---

Step * of Lemma member-eclass-simple-loc-comb-1

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:Id ─→ bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
  (↑e ∈b F(Loc, X)) supposing ((∀loc:Id. ∀as:bag(A).  ((¬↑bag-null(as)) ⇒ (¬↑bag-null(F loc as)))) and (↑e ∈b X))
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : Id ─→ bag(A) ─→ bag(B)
7. X : EClass(A)
8. ↑e ∈b X
9. ∀loc:Id. ∀as:bag(A).  ((¬↑bag-null(as)) ⇒ (¬↑bag-null(F loc as)))
⊢ ↑e ∈b F(Loc, X)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[F:Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].
    (\muparrow{}e  \mmember{}\msubb{}  F(Loc,  X))  supposing 
          ((\mforall{}loc:Id.  \mforall{}as:bag(A).    ((\mneg{}\muparrow{}bag-null(as))  {}\mRightarrow{}  (\mneg{}\muparrow{}bag-null(F  loc  as))))  and 
          (\muparrow{}e  \mmember{}\msubb{}  X))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index