### Nuprl Lemma : es-pred_property

`∀es:EO. ∀e:E.`
`  {(loc(pred(e)) = loc(e) ∈ Id)`
`  ∧ (pred(e) < e)`
`  ∧ (∀e':E. (e' < e) `` ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id)} `
`  supposing ¬↑first(e)`

Proof

Definitions occuring in Statement :  es-first: `first(e)` es-pred: `pred(e)` es-causl: `(e < e')` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` assert: `↑b` uimplies: `b supposing a` guard: `{T}` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` equal: `s = t ∈ T`
Lemmas :  es-pred_property_base assert_wf es-first_wf es-E_wf not_wf event_ordering_wf assert-es-eq-E-base es-eq-E-wf-base es-pred-wf-base bool_wf subtype_base_sq bool_subtype_base iff_imp_equal_bool btrue_wf true_wf es-causl_wf es-pred_wf equal_wf Id_wf es-loc_wf es-dom_wf sq_stable__assert
\mforall{}es:EO.  \mforall{}e:E.
\{(loc(pred(e))  =  loc(e))
\mwedge{}  (pred(e)  <  e)
\mwedge{}  (\mforall{}e':E.  (e'  <  e)  {}\mRightarrow{}  ((e'  =  pred(e))  \mvee{}  (e'  <  pred(e)))  supposing  loc(e')  =  loc(e))\}
supposing  \mneg{}\muparrow{}first(e)

Date html generated: 2015_07_17-AM-08_35_27
Last ObjectModification: 2015_01_27-PM-02_58_41

Home Index