---

Step * of Lemma es-interface-predecessors-cases

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
  (≤(X)(e) ~ if e ∈b X then if first(e) then [e] else ≤(X)(pred(e)) @ [e] fi 
  if first(e) then []
  else ≤(X)(pred(e))
  fi )
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ ≤(X)(e) ~ if e ∈b X then if first(e) then [e] else ≤(X)(pred(e)) @ [e] fi 
if first(e) then []
else ≤(X)(pred(e))
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{}  X  then  if  first(e)  then  [e]  else  \mleq{}(X)(pred(e))  @  [e]  fi 
    if  first(e)  then  []
    else  \mleq{}(X)(pred(e))
    fi  )


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index