---

Step * of Lemma class-output-member-support

∀[Info,T:Type]. ∀[es:EO+(Info)]. ∀[bg:bag(E)]. ∀[x:T]. ∀[X:EClass(T)].
  ↓∃e:E. (e ↓∈ class-output-support(es;bg) ∧ x ∈ X(e)) supposing x ↓∈ class-output(X;es;bg)
BY
{ (Auto
   THEN RepeatFor 2 ((BagMemberD (-1) THEN SquashExRepD))⋅
   THEN (D 0
         THEN (InstConcl [⌈e'⌉]⋅ THENA Auto)
         THEN Auto
         THEN BagMemberD 0
         THEN D 0
         THEN InstConcl [⌈e⌉]⋅
         THEN Auto
         THEN D 0
         THEN Auto
         THEN InstConcl [⌈≤loc(e)⌉]⋅
         THEN Auto)⋅) }

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

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[bg:bag(E)].  \mforall{}[x:T].  \mforall{}[X:EClass(T)].
    \mdownarrow{}\mexists{}e:E.  (e  \mdownarrow{}\mmember{}  class-output-support(es;bg)  \mwedge{}  x  \mmember{}  X(e))  supposing  x  \mdownarrow{}\mmember{}  class-output(X;es;bg)


By

(Auto
  THEN  RepeatFor  2  ((BagMemberD  (-1)  THEN  SquashExRepD))\mcdot{}
  THEN  (D  0
              THEN  (InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  Auto
              THEN  BagMemberD  0
              THEN  D  0
              THEN  InstConcl  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  D  0
              THEN  Auto
              THEN  InstConcl  [\mkleeneopen{}\mleq{}loc(e)\mkleeneclose{}]\mcdot{}
              THEN  Auto)\mcdot{})

---

Home Index