---

Step * of Lemma es-prior-interface-val-unique2

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  ∀[p:E]. (prior(X)(p) = prior(X)(e) ∈ E) supposing ((p <loc e) and (prior(X)(e) <loc p)) supposing ↑e ∈b prior(X)
BY
{ (Auto THEN (InstLemma `es-prior-interface-val` [⌜Info⌝;⌜es⌝;⌜X⌝;⌜e⌝]⋅ THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
6. p : E
7. (prior(X)(e) <loc p)
8. (p <loc e)
9. (prior(X)(e) <loc e) ∧ (↑prior(X)(e) ∈b X) ∧ (∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b X)))
⊢ prior(X)(p) = prior(X)(e) ∈ E

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    \mforall{}[p:E].  (prior(X)(p)  =  prior(X)(e))  supposing  ((p  <loc  e)  and  (prior(X)(e)  <loc  p)) 
    supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)


By

---

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

---

Home Index