---

Step * 1 2 of Lemma es-prior-interface-val-pred

.....falsecase..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
6. (¬↑first(e)) ∧ ((↑pred(e) ∈b X) ∨ (↑pred(e) ∈b prior(X)))
7. ¬↑pred(e) ∈b X
⊢ prior(X)(e) = prior(X)(pred(e)) ∈ E
BY
{ ((Auto THEN D -2) THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
6. ¬↑first(e)
7. ↑pred(e) ∈b prior(X)
8. ¬↑pred(e) ∈b X
⊢ prior(X)(e) = prior(X)(pred(e)) ∈ E

---

Latex:

---

Latex:
.....falsecase..... 
1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  e  :  E
5.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
6.  (\mneg{}\muparrow{}first(e))  \mwedge{}  ((\muparrow{}pred(e)  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}pred(e)  \mmember{}\msubb{}  prior(X)))
7.  \mneg{}\muparrow{}pred(e)  \mmember{}\msubb{}  X
\mvdash{}  prior(X)(e)  =  prior(X)(pred(e))


By

---

Latex:
((Auto  THEN  D  -2)  THEN  Auto)

---

Home Index