---

Step * of Lemma last-event

∀es:EO. ∀e:E.
  ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]
    ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
    ⇒ (∀e'≤e.¬P[e'] ∨ (∃e':E. (e' ≤loc e  c∧ (P[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬P[e'']))))))))
BY
{ InstLemma `previous-event-exists` []  ⋅ }

1
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)
⊢ ∀es:EO. ∀e:E.
    ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]
      ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
      ⇒ (∀e'≤e.¬P[e'] ∨ (∃e':E. (e' ≤loc e  c∧ (P[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬P[e'']))))))))

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.
    \mforall{}[P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a]))
        {}\mRightarrow{}  (\mforall{}e'\mleq{}e.\mneg{}P[e']
              \mvee{}  (\mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  (P[e']  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}P[e'']))))))))


By

InstLemma  `previous-event-exists`  []    \mcdot{}

---

Home Index