---

Step * 1 of Lemma primed-class-opt-exists


1. Info : Type
2. B : Type
3. es : EO+(Info)
4. X : EClass(B)
5. init : Id ⟶ bag(B)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (↓∃x:B. x ↓∈ init loc(e1)) ⇒ (↓∃b:B. b ∈ Prior(X)?init(e1)))
8. ¬↑first(e)
9. x : B@i
10. x ↓∈ init loc(e)@i
11. #(X es pred(e)) ≤ 0
12. ↓∃b:B. b ∈ Prior(X)?init(pred(e))
⊢ ↓∃b:B. b ↓∈ Prior(X)?init es pred(e)
BY
{ (SquashExRepD THEN Unfold `classrel` (-1) THEN D 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(B)
5.  init  :  Id  {}\mrightarrow{}  bag(B)
6.  e  :  E@i
7.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}x:B.  x  \mdownarrow{}\mmember{}  init  loc(e1))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}b:B.  b  \mmember{}  Prior(X)?init(e1)))
8.  \mneg{}\muparrow{}first(e)
9.  x  :  B@i
10.  x  \mdownarrow{}\mmember{}  init  loc(e)@i
11.  \#(X  es  pred(e))  \mleq{}  0
12.  \mdownarrow{}\mexists{}b:B.  b  \mmember{}  Prior(X)?init(pred(e))
\mvdash{}  \mdownarrow{}\mexists{}b:B.  b  \mdownarrow{}\mmember{}  Prior(X)?init  es  pred(e)


By

---

Latex:
(SquashExRepD  THEN  Unfold  `classrel`  (-1)  THEN  D  0  THEN  Auto)\mcdot{}

---

Home Index