Nuprl Lemma : event_ordering_properties

eo:EO
  ((∀x,y:es-base-E(eo).  ((x < y)  es-rank(eo;x) < es-rank(eo;y)))
  ∧ (∀e:es-base-E(eo). (loc(pred1(e)) loc(e) ∈ Id))
  ∧ (∀e:es-base-E(eo). (e < pred1(e))))
  ∧ (∀e,x:es-base-E(eo).  ((x < e)  (loc(x) loc(e) ∈ Id)  ((pred1(e) < e) ∧ (pred1(e) < x)))))
  ∧ (∀x,y,z:es-base-E(eo).  ((x < y)  (y < z)  (x < z)))
  ∧ (∀e1,e2:es-base-E(eo).
       ((e1 < e2) ⇐⇒ ↑es-locless(eo;e1;e2)) ∧ ((¬(e1 < e2))  (e2 < e1))  (e1 e2 ∈ es-base-E(eo))) 
       supposing loc(e1) loc(e2) ∈ Id))


Proof




Definitions occuring in Statement :  es-rank: es-rank(es;e) es-locless: es-locless(es;e1;e2) 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 assert: b less_than: a < b uimplies: supposing a all: x:A. B[x] iff: ⇐⇒ Q not: ¬A implies:  Q and: P ∧ Q equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] event_ordering: EO uall: [x:A]. B[x] member: t ∈ T sq_stable: SqStable(P) implies:  Q squash: T eo_axioms: eo_axioms(r) es-base-E: es-base-E(es) es-causl: (e < e') es-locless: es-locless(es;e1;e2) es-loc: loc(e) es-base-pred: pred1(e) es-rank: es-rank(es;e)

Latex:
\mforall{}eo:EO
    ((\mforall{}x,y:es-base-E(eo).    ((x  <  y)  {}\mRightarrow{}  es-rank(eo;x)  <  es-rank(eo;y)))
    \mwedge{}  (\mforall{}e:es-base-E(eo).  (loc(pred1(e))  =  loc(e)))
    \mwedge{}  (\mforall{}e:es-base-E(eo).  (\mneg{}(e  <  pred1(e))))
    \mwedge{}  (\mforall{}e,x:es-base-E(eo).    ((x  <  e)  {}\mRightarrow{}  (loc(x)  =  loc(e))  {}\mRightarrow{}  ((pred1(e)  <  e)  \mwedge{}  (\mneg{}(pred1(e)  <  x)))))
    \mwedge{}  (\mforall{}x,y,z:es-base-E(eo).    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z)))
    \mwedge{}  (\mforall{}e1,e2:es-base-E(eo).
              ((e1  <  e2)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(eo;e1;e2))  \mwedge{}  ((\mneg{}(e1  <  e2))  {}\mRightarrow{}  (\mneg{}(e2  <  e1))  {}\mRightarrow{}  (e1  =  e2)) 
              supposing  loc(e1)  =  loc(e2)))



Date html generated: 2016_05_16-AM-09_14_33
Last ObjectModification: 2016_01_17-PM-01_31_24

Theory : new!event-ordering


Home Index