---

Step * of Lemma es-interface-predecessors-step

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E(X)].
  (≤(X)(e) = if e ∈b prior(X) then ≤(X)(prior(X)(e)) @ [e] else [e] fi  ∈ ({a:E(X)| loc(a) = loc(e) ∈ Id}  List))
BY
{ (InstLemma `es-interface-predecessors-step-sq` []
   THEN RepeatFor 3 (ParallelLast')
   THEN ParallelLast
   THEN HypSubst' (-1) 0
   THEN RepeatFor 2 ((AutoSplit THENA Auto))) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `es-interface-predecessors-step-sq`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  ParallelLast
  THEN  HypSubst'  (-1)  0
  THEN  RepeatFor  2  ((AutoSplit  THENA  Auto)))

---

Home Index