---

Step * 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)))
⊢ ↑e ∈b F(Loc, X)
BY
{ (InstHyp [⌜loc(e)⌝;⌜X es e⌝] (-1)⋅
   THENA (Auto
          THEN (D 0 THENA Auto)
          THEN (FLemma `assert-bag-null-sq` [-1] THENA (Auto THEN DoSubsume THEN Auto))
          THEN (RWO "member-eclass-iff-size" (-4) THENA Auto)
          THEN RWO "-1" (-4)
          THEN Reduce (-4)
          THEN 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)))
10. ¬↑bag-null(F loc(e) (X es e))
⊢ ↑e ∈b F(Loc, X)

---

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)))
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  F(Loc,  X)


By

---

Latex:
(InstHyp  [\mkleeneopen{}loc(e)\mkleeneclose{};\mkleeneopen{}X  es  e\mkleeneclose{}]  (-1)\mcdot{}
  THENA  (Auto
                THEN  (D  0  THENA  Auto)
                THEN  (FLemma  `assert-bag-null-sq`  [-1]  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
                THEN  (RWO  "member-eclass-iff-size"  (-4)  THENA  Auto)
                THEN  RWO  "-1"  (-4)
                THEN  Reduce  (-4)
                THEN  Auto)
  )

---

Home Index