---

Step * 1 1 of Lemma member-eclass-simple-loc-comb-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)))
10. ¬↑bag-null(F loc(e) (X es e))
⊢ ↑e ∈b F(Loc, X)
BY
{ (All (RepUR ``simple-loc-comb-1 simple-loc-comb member-eclass``)⋅
   THEN (RWO "null-bag-size<" 0 THENA Auto)
   THEN (RWO "null-bag-size<" (-3) THENA Auto)
   THEN Repeat (AllPushDown)
   THEN BackThruSomeHyp)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  e  :  E
6.  F  :  Id  {}\mrightarrow{}  bag(A)  {}\mrightarrow{}  bag(B)
7.  X  :  EClass(A)
8.  \muparrow{}e  \mmember{}\msubb{}  X
9.  \mforall{}loc:Id.  \mforall{}as:bag(A).    ((\mneg{}\muparrow{}bag-null(as))  {}\mRightarrow{}  (\mneg{}\muparrow{}bag-null(F  loc  as)))
10.  \mneg{}\muparrow{}bag-null(F  loc(e)  (X  es  e))
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  F(Loc,  X)


By

---

Latex:
(All  (RepUR  ``simple-loc-comb-1  simple-loc-comb  member-eclass``)\mcdot{}
  THEN  (RWO  "null-bag-size<"  0  THENA  Auto)
  THEN  (RWO  "null-bag-size<"  (-3)  THENA  Auto)
  THEN  Repeat  (AllPushDown)
  THEN  BackThruSomeHyp)\mcdot{}

---

Home Index