---

Step * of Lemma es-interface-predecessors-nil

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  (≤(X)(pred(e)) ~ []) supposing ((¬↑first(e)) and (¬↑e ∈b prior(X)))
BY
{ ((UnivCD THENA Auto)
   THEN (GenConclAtAddr [1]
         THEN (D -2 THENA Auto)
         THEN Try (Trivial)
         THEN D -5
         THEN RWO "is-prior-interface" 0
         THEN Auto)⋅
   ) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ¬↑first(e)
6. u : {a:E(X)| loc(a) = loc(pred(e)) ∈ Id} 
7. v : {a:E(X)| loc(a) = loc(pred(e)) ∈ Id}  List
8. ≤(X)(pred(e)) = [u / v] ∈ ({a:E(X)| loc(a) = loc(pred(e)) ∈ Id}  List)@i
⊢ ∃e':E. ((e' <loc e) ∧ (↑e' ∈b X))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (\mleq{}(X)(pred(e))  \msim{}  [])  supposing  ((\mneg{}\muparrow{}first(e))  and  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  prior(X)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (GenConclAtAddr  [1]
              THEN  (D  -2  THENA  Auto)
              THEN  Try  (Trivial)
              THEN  D  -5
              THEN  RWO  "is-prior-interface"  0
              THEN  Auto)\mcdot{}
  )

---

Home Index