---

Step * of Lemma member-class-le-before

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].
  uiff(v ↓∈ class-le-before(X;es;e);↓∃e':E. (e' ≤loc e  ∧ v ∈ X(e')))
BY
{ (((UnivCD THENM Unfold `class-le-before` 0 THENM Assert ⌈≤loc(e) ∈ bag(E)⌉⋅) THENA Auto)
   THEN Auto
   THEN ((BagMemberD (-1) THEN Fold `classrel` (-1)) ORELSE (BagMemberD 0 THEN Fold `classrel` 0))
   THEN RepeatFor 3 (ParallelLast)) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : T
7. ≤loc(e) ∈ bag(E)
8. e' : E
9. v ∈ X(e')
10. e' ↓∈ ≤loc(e)
⊢ e' ≤loc e 

2
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : T
7. ≤loc(e) ∈ bag(E)
8. e' : E
9. v ∈ X(e')
10. e' ≤loc e 
⊢ e' ↓∈ ≤loc(e)

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].
    uiff(v  \mdownarrow{}\mmember{}  class-le-before(X;es;e);\mdownarrow{}\mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  v  \mmember{}  X(e')))


By

(((UnivCD  THENM  Unfold  `class-le-before`  0  THENM  Assert  \mkleeneopen{}\mleq{}loc(e)  \mmember{}  bag(E)\mkleeneclose{}\mcdot{})  THENA  Auto)
  THEN  Auto
  THEN  ((BagMemberD  (-1)  THEN  Fold  `classrel`  (-1))  ORELSE  (BagMemberD  0  THEN  Fold  `classrel`  0))
  THEN  RepeatFor  3  (ParallelLast))

---

Home Index