---

Step * 1 of Lemma es-first-at-since_wf


1. es : EO
2. i : Id
3. e' : E
4. P : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
5. R : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
⊢ (loc(e') = i ∈ Id) ∧ (P[e'] ∧ (¬R[e'])) ∧ ∀e'@0<e'.P[e'@0] ⇒ (∃e'':E. (e'@0 ≤loc e''  ∧ (e'' <loc e') ∧ R[e''])) ∈ ℙ
BY
{ (Unfold `and` 0 THEN Fold `cand` 0 THEN Auto THEN ExRepD THEN Auto) }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  e'  :  E
4.  P  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
5.  R  :  \{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}
\mvdash{}  (loc(e')  =  i)
    \mwedge{}  (P[e']  \mwedge{}  (\mneg{}R[e']))
    \mwedge{}  \mforall{}e'@0<e'.P[e'@0]  {}\mRightarrow{}  (\mexists{}e'':E.  (e'@0  \mleq{}loc  e''    \mwedge{}  (e''  <loc  e')  \mwedge{}  R[e'']))  \mmember{}  \mBbbP{}


By

(Unfold  `and`  0  THEN  Fold  `cand`  0  THEN  Auto  THEN  ExRepD  THEN  Auto)

---

Home Index