Nuprl Lemma : es-base-pred-properties

es:EO. ∀e:es-base-E(es).
  ((loc(pred1(e)) loc(e) ∈ Id)
  ∧ (e < pred1(e)))
  ∧ (∀x:es-base-E(es). ((x < e)  (loc(x) loc(e) ∈ Id)  ((pred1(e) < e) ∧ (pred1(e) < x))))))


Proof




Definitions occuring in Statement :  es-causl: (e < e') es-base-pred: pred1(e) es-loc: loc(e) es-base-E: es-base-E(es) event_ordering: EO Id: Id all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T and: P ∧ Q uall: [x:A]. B[x]

Latex:
\mforall{}es:EO.  \mforall{}e:es-base-E(es).
    ((loc(pred1(e))  =  loc(e))
    \mwedge{}  (\mneg{}(e  <  pred1(e)))
    \mwedge{}  (\mforall{}x:es-base-E(es).  ((x  <  e)  {}\mRightarrow{}  (loc(x)  =  loc(e))  {}\mRightarrow{}  ((pred1(e)  <  e)  \mwedge{}  (\mneg{}(pred1(e)  <  x))))))



Date html generated: 2016_05_16-AM-09_14_35
Last ObjectModification: 2015_12_28-PM-09_58_19

Theory : new!event-ordering


Home Index