---

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


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. lifting-like(A;F)
9. single-valued-classrel(es;X;A)
10. ↑e ∈b F|X|
⊢ (↑e ∈b X) ∧ (¬↑bag-null(F {X@e}))
BY
{ ((Unfold `lifting-like` 8 THEN D 8)
   THEN (RepUR ``member-eclass simple-comb-1 simple-comb`` (-1))⋅
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN Assert ⌈¬((X es e) = {} ∈ bag(A))⌉⋅) }

1
.....assertion..... 
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F as) ⇐⇒ ↑bag-null(F {x})))
9. ↑bag-null(F {})
10. single-valued-classrel(es;X;A)
11. ¬(#(F (X es e)) = 0 ∈ ℤ)
⊢ ¬((X es e) = {} ∈ bag(A))

2
1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. e : E
6. F : bag(A) ─→ bag(B)
7. X : EClass(A)
8. ∀as:bag(A). ∀x:A.  (single-valued-bag(as;A) ⇒ x ↓∈ as ⇒ (↑bag-null(F as) ⇐⇒ ↑bag-null(F {x})))
9. ↑bag-null(F {})
10. single-valued-classrel(es;X;A)
11. ¬(#(F (X es e)) = 0 ∈ ℤ)
12. ¬((X es e) = {} ∈ bag(A))
⊢ (↑e ∈b X) ∧ (¬↑bag-null(F {X@e}))

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  e  :  E
6.  F  :  bag(A)  {}\mrightarrow{}  bag(B)
7.  X  :  EClass(A)
8.  lifting-like(A;F)
9.  single-valued-classrel(es;X;A)
10.  \muparrow{}e  \mmember{}\msubb{}  F|X|
\mvdash{}  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\mneg{}\muparrow{}bag-null(F  \{X@e\}))


By

---

Latex:
((Unfold  `lifting-like`  8  THEN  D  8)
  THEN  (RepUR  ``member-eclass  simple-comb-1  simple-comb``  (-1))\mcdot{}
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  Assert  \mkleeneopen{}\mneg{}((X  es  e)  =  \{\})\mkleeneclose{}\mcdot{})

---

Home Index