---

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

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  ∀[p:E]
    p = prior(X)(e) ∈ E supposing (p <loc e) ∧ (↑p ∈b X) ∧ (∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))) 
  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. (p <loc e)
8. ↑p ∈b X
9. ∀e'':E. ((e'' <loc e) ⇒ (p <loc e'') ⇒ (¬↑e'' ∈b X))
10. (prior(X)(e) <loc e) ∧ (↑prior(X)(e) ∈b X) ∧ (∀e'':E. ((e'' <loc e) ⇒ (prior(X)(e) <loc e'') ⇒ (¬↑e'' ∈b 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]
        p  =  prior(X)(e) 
        supposing  (p  <loc  e)  \mwedge{}  (\muparrow{}p  \mmember{}\msubb{}  X)  \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e)  {}\mRightarrow{}  (p  <loc  e'')  {}\mRightarrow{}  (\mneg{}\muparrow{}e''  \mmember{}\msubb{}  X))) 
    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)\mcdot{})

---

Home Index