### Nuprl Lemma : es-pred_property_base

`∀es:EO. ∀e:es-base-E(es).`
`  ((loc(pred(e)) = loc(e) ∈ Id)`
`  ∧ ((pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es)))`
`  ∧ (∀e':E. (e' < e) `` ((e' = pred(e) ∈ es-base-E(es)) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id))`

Proof

Definitions occuring in Statement :  es-pred: `pred(e)` es-causl: `(e < e')` es-loc: `loc(e)` es-E: `E` es-base-E: `es-base-E(es)` event_ordering: `EO` Id: `Id` uimplies: `b supposing a` all: `∀x:A. B[x]` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` equal: `s = t ∈ T`
Lemmas :  es-pred-wf-base decidable__equal-es-base-E es-causl-wf-base es-pred-less-base equal_wf es-base-E_wf es-loc-wf-base Id_wf es-loc_wf es-E_wf decidable__es-causl-same-loc es-pred-loc-base iff_weakening_equal es-pred-maximal-base es-causl-total-base
\mforall{}es:EO.  \mforall{}e:es-base-E(es).
((loc(pred(e))  =  loc(e))
\mwedge{}  ((pred(e)  <  e)  \mvee{}  (pred(e)  =  e))
\mwedge{}  (\mforall{}e':E.  (e'  <  e)  {}\mRightarrow{}  ((e'  =  pred(e))  \mvee{}  (e'  <  pred(e)))  supposing  loc(e')  =  loc(e)))

Date html generated: 2015_07_17-AM-08_35_23
Last ObjectModification: 2015_02_04-AM-07_07_22

Home Index