---

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

∀[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 )
  ∈ ({a:E(X)| loc(a) = loc(e) ∈ Id}  List))
BY
{ (Auto THEN (BLemma `list-equal-set` THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ (∀a∈≤(X)(e).loc(a) = loc(e) ∈ Id)

2
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
⊢ ≤(X)(e) = (if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi ) ∈ (E(X) List)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[e:E].
    (\mleq{}(X)(e)  =  (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:
(Auto  THEN  (BLemma  `list-equal-set`  THENA  Auto))

---

Home Index