---

Step * of Lemma member-eclass-eclass0

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ⟶ B ⟶ bag(C)]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(↑e ∈b (f o X);(↑e ∈b X) ∧ (¬↑bag-null(f loc(e) X@e))) supposing single-valued-classrel(es;X;B)
BY
{ (Auto
   THEN (All(RWO "assert-member-eclass") THENA Auto)
   THEN TrySquashExRepD (-1)
   THEN Try (DNot 0⋅)
   THEN Auto
   THEN ExRepD
   THEN All MaUseClassRel
   THEN Try (Complete ((D 0 THEN InstConcl [⌜b⌝]⋅ THEN Auto)))
   THEN Try (Complete (((RWO "assert-member-eclass" 0 THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN Auto)))) }

1
1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. f : Id ⟶ B ⟶ bag(C)
6. es : EO+(Info)
7. e : E
8. single-valued-classrel(es;X;B)
9. v : C
10. b : B
11. b ∈ X(e)
12. v ↓∈ f loc(e) b
13. ↑bag-null(f loc(e) X@e)@i
⊢ False

2
1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. f : Id ⟶ B ⟶ bag(C)
6. es : EO+(Info)
7. e : E
8. single-valued-classrel(es;X;B)
9. v : B
10. v ∈ X(e)
11. ¬↑bag-null(f loc(e) X@e)
⊢ ↓∃v:C. v ∈ (f o X)(e)

---

Latex:

---

Latex:
\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  bag(C)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  (f  o  X);(\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (\mneg{}\muparrow{}bag-null(f  loc(e)  X@e))) 
    supposing  single-valued-classrel(es;X;B)


By

---

Latex:
(Auto
  THEN  (All(RWO  "assert-member-eclass")  THENA  Auto)
  THEN  TrySquashExRepD  (-1)
  THEN  Try  (DNot  0\mcdot{})
  THEN  Auto
  THEN  ExRepD
  THEN  All  MaUseClassRel
  THEN  Try  (Complete  ((D  0  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  (((RWO  "assert-member-eclass"  0  THENA  Auto)
                                            THEN  RepeatFor  2  (ParallelLast)
                                            THEN  Auto))))

---

Home Index