---

Step * of Lemma class-pred-cases

∀[Info,T:Type].
  ∀X:EClass(T). ∀es:EO+(Info). ∀e:E.
    (∃e'<e.((↓∃v:T. v ∈ X(e')) ∧ ∀e''<e.(↓∃v:T. v ∈ X(e'')) ⇒ e'' ≤loc e' )
    ∧ (class-pred(X;es;e) = (inl e') ∈ (E + Top))
    ∨ (∀e'<e.∀v:T. (¬v ∈ X(e')) ∧ (class-pred(X;es;e) = (inr ⋅ ) ∈ (E + Top))))
BY
{ Assert ⌜∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))⌝⋅ }

1
.....assertion..... 
∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))

2
1. ∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))
⊢ ∀[Info,T:Type].
    ∀X:EClass(T). ∀es:EO+(Info). ∀e:E.
      (∃e'<e.((↓∃v:T. v ∈ X(e')) ∧ ∀e''<e.(↓∃v:T. v ∈ X(e'')) ⇒ e'' ≤loc e' )
      ∧ (class-pred(X;es;e) = (inl e') ∈ (E + Top))
      ∨ (∀e'<e.∀v:T. (¬v ∈ X(e')) ∧ (class-pred(X;es;e) = (inr ⋅ ) ∈ (E + Top))))

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].
    \mforall{}X:EClass(T).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\mexists{}e'<e.((\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e'))  \mwedge{}  \mforall{}e''<e.(\mdownarrow{}\mexists{}v:T.  v  \mmember{}  X(e''))  {}\mRightarrow{}  e''  \mleq{}loc  e'  )
        \mwedge{}  (class-pred(X;es;e)  =  (inl  e'))
        \mvee{}  (\mforall{}e'<e.\mforall{}v:T.  (\mneg{}v  \mmember{}  X(e'))  \mwedge{}  (class-pred(X;es;e)  =  (inr  \mcdot{}  ))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}[T:Type].  \mforall{}[b:bag(T)].    (\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  b  \mLeftarrow{}{}\mRightarrow{}  0  <  \#(b))\mkleeneclose{}\mcdot{}

---

Home Index