---

Step * of Lemma es-first-at-since'_wf

∀[es:EO]. ∀[i:Id]. ∀[e':E]. ∀[P,R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ].  (es-first-at-since'(es;i;e';e.R[e];e.P[e]) ∈ ℙ)
BY
{ ((Auto THEN Unfold_o (ioid Obid: es-first-at-since') 0⋅ THEN (UnivCD THENA Auto))
   THEN Unfolds ``and alle-lt`` 0
   THEN Fold `cand` 0
   THEN Auto
   THEN MemTypeCD
   THEN ExRepD
   THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].  \mforall{}[e':E].  \mforall{}[P,R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].
    (es-first-at-since'(es;i;e';e.R[e];e.P[e])  \mmember{}  \mBbbP{})


By

((Auto  THEN  Unfold\_o  (ioid  Obid:  es-first-at-since')  0\mcdot{}  THEN  (UnivCD  THENA  Auto))
  THEN  Unfolds  ``and  alle-lt``  0
  THEN  Fold  `cand`  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  ExRepD
  THEN  Auto)

---

Home Index