Nuprl Definition : eo_axioms

eo_axioms(r) ==
  (∀x,y:r."E".  ((↓r."<y)  r."rank" x < r."rank" y))
  ∧ (∀e:r."E". ((r."loc" (r."pred" e)) (r."loc" e) ∈ Id))
  ∧ (∀e:r."E". (¬↓r."<(r."pred" e)))
  ∧ (∀e,x:r."E".
       ((↓r."<e)  ((r."loc" x) (r."loc" e) ∈ Id)  ((↓(r."pred" e) r."<e) ∧ (¬↓(r."pred" e) r."<x))))
  ∧ (∀x,y,z:r."E".  ((↓r."<y)  (↓r."<z)  (↓r."<z)))
  ∧ (∀e1,e2:r."E".
       (↓e1 r."<e2 ⇐⇒ ↑(e1 r."locless" e2)) ∧ ((¬↓e1 r."<e2)  (¬↓e2 r."<e1)  (e1 e2 ∈ r."E")) 
       supposing (r."loc" e1) (r."loc" e2) ∈ Id)



Definitions occuring in Statement :  Id: Id assert: b less_than: a < b uimplies: supposing a infix_ap: y all: x:A. B[x] iff: ⇐⇒ Q not: ¬A squash: T implies:  Q and: P ∧ Q apply: a token: "$token" equal: t ∈ T record-select: r.x
FDL editor aliases :  eo_axioms

Latex:
eo\_axioms(r)  ==
    (\mforall{}x,y:r."E".    ((\mdownarrow{}x  r."<"  y)  {}\mRightarrow{}  r."rank"  x  <  r."rank"  y))
    \mwedge{}  (\mforall{}e:r."E".  ((r."loc"  (r."pred"  e))  =  (r."loc"  e)))
    \mwedge{}  (\mforall{}e:r."E".  (\mneg{}\mdownarrow{}e  r."<"  (r."pred"  e)))
    \mwedge{}  (\mforall{}e,x:r."E".
              ((\mdownarrow{}x  r."<"  e)
              {}\mRightarrow{}  ((r."loc"  x)  =  (r."loc"  e))
              {}\mRightarrow{}  ((\mdownarrow{}(r."pred"  e)  r."<"  e)  \mwedge{}  (\mneg{}\mdownarrow{}(r."pred"  e)  r."<"  x))))
    \mwedge{}  (\mforall{}x,y,z:r."E".    ((\mdownarrow{}x  r."<"  y)  {}\mRightarrow{}  (\mdownarrow{}y  r."<"  z)  {}\mRightarrow{}  (\mdownarrow{}x  r."<"  z)))
    \mwedge{}  (\mforall{}e1,e2:r."E".
              (\mdownarrow{}e1  r."<"  e2  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(e1  r."locless"  e2))  \mwedge{}  ((\mneg{}\mdownarrow{}e1  r."<"  e2)  {}\mRightarrow{}  (\mneg{}\mdownarrow{}e2  r."<"  e1)  {}\mRightarrow{}  (e1  =  e2)) 
              supposing  (r."loc"  e1)  =  (r."loc"  e2))



Date html generated: 2016_05_16-AM-09_13_31
Last ObjectModification: 2014_02_20-PM-10_35_16

Theory : new!event-ordering


Home Index