---

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

.....truecase..... 
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) = pred(e) ∈ E
BY
{ (InstLemma `es-prior-interface-val` [⌈Info⌉;⌈es⌉;⌈X⌉;⌈e⌉]⋅ 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 X) ∨ (↑pred(e) ∈b prior(X))
8. ↑pred(e) ∈b X
9. (prior(X)(e) <loc e)
10. ↑prior(X)(e) ∈b X
11. ∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X))
⊢ prior(X)(e) = pred(e) ∈ E

---

Latex:

---

Latex:
.....truecase..... 
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.  \muparrow{}pred(e)  \mmember{}\msubb{}  X
\mvdash{}  prior(X)(e)  =  pred(e)


By

---

Latex:
(InstLemma  `es-prior-interface-val`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index