---

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


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. lifting-like(A;F loc(e))
9. single-valued-classrel(es;X;A)
10. (↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e}))
⊢ ↑e ∈b F(Loc, X)
BY
{ ((RepUR ``member-eclass simple-loc-comb-1 simple-loc-comb`` 0)⋅
   THEN ((RW assert_pushdownC 0)⋅ THENA Auto)
   THEN Unfold `lifting-like` 8
   THEN ((D 8 THEN InstHyp [⌈X es e⌉; ⌈X@e⌉] 8⋅) 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. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F loc(e) as) ⇐⇒ ↑bag-null(F loc(e) {x})))
9. ↑bag-null(F loc(e) {})
10. single-valued-classrel(es;X;A)
11. ↑e ∈b X
12. ¬↑bag-null(F loc(e) {X@e})
⊢ single-valued-bag(X es e;A)

2
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. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F loc(e) as) ⇐⇒ ↑bag-null(F loc(e) {x})))
9. ↑bag-null(F loc(e) {})
10. single-valued-classrel(es;X;A)
11. ↑e ∈b X
12. ¬↑bag-null(F loc(e) {X@e})
⊢ X@e ↓∈ X es e

3
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. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F loc(e) as) ⇐⇒ ↑bag-null(F loc(e) {x})))
9. ↑bag-null(F loc(e) {})
10. single-valued-classrel(es;X;A)
11. (↑e ∈b X) ∧ (¬↑bag-null(F loc(e) {X@e}))
12. ↑bag-null(F loc(e) (X es e)) ⇐⇒ ↑bag-null(F loc(e) {X@e})
⊢ ¬(#(F loc(e) (X es e)) = 0 ∈ ℤ)

---

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.  lifting-like(A;F  loc(e))
9.  single-valued-classrel(es;X;A)
10.  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\mneg{}\muparrow{}bag-null(F  loc(e)  \{X@e\}))
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  F(Loc,  X)


By

---

Latex:
((RepUR  ``member-eclass  simple-loc-comb-1  simple-loc-comb``  0)\mcdot{}
  THEN  ((RW  assert\_pushdownC  0)\mcdot{}  THENA  Auto)
  THEN  Unfold  `lifting-like`  8
  THEN  ((D  8  THEN  InstHyp  [\mkleeneopen{}X  es  e\mkleeneclose{};  \mkleeneopen{}X@e\mkleeneclose{}]  8\mcdot{})  THENA  Auto))\mcdot{}

---

Home Index