---

Step * 1 of Lemma es-local-pred_wf2


∀Info:Type. ∀es:EO+(Info). ∀e:E. ∀P:{e':E| (e' <loc e)}  ─→ 𝔹.
  (last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))})))
BY
{ ((D 0 THENA Auto) THEN CausalInd' THEN (D 0 THENA Auto)) }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. e : E@i
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| (e' <loc e1)}  ─→ 𝔹
           (last(P) e1 ∈ (∃e':{E
            ((e' <loc e1) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e1) ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| ((e' <loc e1) ∧ (↑(P e')))})))))
5. P : {e':E| (e' <loc e)}  ─→ 𝔹@i
⊢ last(P) e ∈ (∃e':{E| ((e' <loc e) ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑(P e')))}))

---

Latex:

---

Latex:

\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
    (last(P)  e  \mmember{}  (\mexists{}e':\{E|  ((e'  <loc  e)
                                                \mwedge{}  (\muparrow{}(P  e'))
                                                \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}(P  e'')))))\})
      \mvee{}  (\mneg{}(\mexists{}e':\{E|  ((e'  <loc  e)  \mwedge{}  (\muparrow{}(P  e')))\})))


By

---

Latex:
((D  0  THENA  Auto)  THEN  CausalInd'  THEN  (D  0  THENA  Auto))

---

Home Index