---

Step * of Lemma es-interface-pred_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)].  (X-pred ∈ sys-antecedent(es;X))
BY
{ (Unfold `es-interface-pred` 0 THEN Auto THEN (MemTypeCD THEN Auto) THEN Reduce 0) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. x : E(X)@i
⊢ if x ∈b prior(X) then prior(X)(x) else x fi  c≤ x

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].    (X-pred  \mmember{}  sys-antecedent(es;X))


By

---

Latex:
(Unfold  `es-interface-pred`  0  THEN  Auto  THEN  (MemTypeCD  THEN  Auto)  THEN  Reduce  0)

---

Home Index