---

Step * 2 of Lemma until-class-simple-comb


1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. ∀e'<e.∀v:Top. (¬v ∈ Y(e'))
8. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
9. ¬(∀v:Top. (¬v ∈ Prior(Y)(e)))
⊢ (X es e) = {} ∈ bag(A)
BY
{ (D (-1) THEN Auto THEN (D 0 THENA Auto)) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(Top)
5. es : EO+(Info)
6. e : E
7. ∀e'<e.∀v:Top. (¬v ∈ Y(e'))
8. class-pred(Y;es;e) = (inr ⋅ ) ∈ (E + Top)
9. v : Top@i
10. v ∈ Prior(Y)(e)@i
⊢ False

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  X  :  EClass(A)
4.  Y  :  EClass(Top)
5.  es  :  EO+(Info)
6.  e  :  E
7.  \mforall{}e'<e.\mforall{}v:Top.  (\mneg{}v  \mmember{}  Y(e'))
8.  class-pred(Y;es;e)  =  (inr  \mcdot{}  )
9.  \mneg{}(\mforall{}v:Top.  (\mneg{}v  \mmember{}  Prior(Y)(e)))
\mvdash{}  (X  es  e)  =  \{\}


By

---

Latex:
(D  (-1)  THEN  Auto  THEN  (D  0  THENA  Auto))

---

Home Index