---

Step * of Lemma es-interface-predecessors-step-sq

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  (≤(X)(e) ~ if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi )
BY
{ (UniformUnivCD Auto THEN Repeat (MoveToConcl (-1))) }

1
∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.
  (≤(X)(e) ~ if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi )

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (\mleq{}(X)(e)  \msim{}  if  e  \mmember{}\msubb{}  prior(X)  then  \mleq{}(X)(prior(X)(e))  else  []  fi    @  if  e  \mmember{}\msubb{}  X  then  [e]  else  []  fi  )


By

---

Latex:
(UniformUnivCD  Auto  THEN  Repeat  (MoveToConcl  (-1)))

---

Home Index