---

Step * 2 of Lemma class-pred-cases


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))))
BY
{ (Auto
   THEN Unfold `class-pred` 0
   THEN GenConclAtAddr [2;2;2]
   THEN All Reduce
   THEN Auto
   THEN D -1
   THEN ParallelOp -2
   THEN Auto) }

1
1. ∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))
2. [Info] : Type
3. [T] : Type
4. X : EClass(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. x : ∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))))}@i
8. (last(λe'.0 <z #(X es e')) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')))})))
⊢ ∃e'<e.((↓∃v:T. v ∈ X(e')) ∧ ∀e''<e.(↓∃v:T. v ∈ X(e'')) ⇒ e'' ≤loc e' ) ∧ ((inl x) = (inl e') ∈ (E + Top))

2
1. ∀[T:Type]. ∀[b:bag(T)].  (↓∃x:T. x ↓∈ b ⇐⇒ 0 < #(b))
2. [Info] : Type
3. [T] : Type
4. X : EClass(T)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. y : ¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')))})@i
8. (last(λe'.0 <z #(X es e')) e)
= (inr y )
∈ ((∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')))})))
⊢ ∀e'<e.∀v:T. (¬v ∈ X(e'))

---

Latex:

---

Latex:

1.  \mforall{}[T:Type].  \mforall{}[b:bag(T)].    (\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  b  \mLeftarrow{}{}\mRightarrow{}  0  <  \#(b))
\mvdash{}  \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:
(Auto
  THEN  Unfold  `class-pred`  0
  THEN  GenConclAtAddr  [2;2;2]
  THEN  All  Reduce
  THEN  Auto
  THEN  D  -1
  THEN  ParallelOp  -2
  THEN  Auto)

---

Home Index