---

Step * 1 1 2 of Lemma last-event


1. ∀es:EO. ∀i:Id.
     ∀[R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]
       ∀e:E
         ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)
         ⇒ (∃e':E. (e' ≤loc e  c∧ R[e']))
            ⇒ (∃e':E. (e' ≤loc e  c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬R[e''])))))) 
            supposing loc(e) = i ∈ Id)
2. es : EO@i'
3. e : E@i
4. [P] : {a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ
5. ∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a])@i
6. ¬(∃e':E. (e' ≤loc e  c∧ P[e']))
⊢ ∀e'≤e.¬P[e']
BY
{ ((D 0 THEN Auto) THEN ParallelOp -3 THEN Auto) }

---

Latex:



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


By

((D  0  THEN  Auto)  THEN  ParallelOp  -3  THEN  Auto)

---

Home Index