Nuprl Lemma : es-local-pred_wf

`∀[Info:Type]. ∀[es:EO+(Info)]. ∀[P:E ─→ 𝔹].`
`  (last(P) ∈ e: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')))}))))`

Proof

Definitions occuring in Statement :  es-local-pred: `last(P)` event-ordering+: `EO+(Info)` es-locl: `(e <loc e')` es-E: `E` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` sq_exists: `∃x:{A| B[x]}` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` member: `t ∈ T` apply: `f a` function: `x:A ─→ B[x]` universe: `Type`
Lemmas :  es-local-pred_wf2 es-E_wf event-ordering+_subtype bool_wf event-ordering+_wf subtype_rel_dep_function es-locl_wf subtype_rel_self set_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[P:E  {}\mrightarrow{}  \mBbbB{}].
(last(P)  \mmember{}  e:E  {}\mrightarrow{}  ((\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')))\}))))

Date html generated: 2015_07_20-PM-03_57_20
Last ObjectModification: 2015_01_27-PM-09_54_53

Home Index