Nuprl Definition : global-order-preserving

global-order-preserving(es;X;f) ==
  ∀a,a':E(X).
    (a is f*(a')
    ⇒ (∀b,b':E(X).
          (b is f*(b') ⇒ (loc(a) = loc(b) ∈ Id) ⇒ (loc(a') = loc(b') ∈ Id) ⇒ ((a <loc b) ⇐⇒ (a' <loc b')))))

Definitions occuring in Statement : es-E-interface: E(X), es-locl: (e <loc e'), es-loc: loc(e), Id: Id, all: ∀x:A. B[x], iff: P ⇐⇒ Q, implies: P ⇒ Q, equal: s = t ∈ T, fun-connected: y is f*(x)
FDL editor aliases : global-order-preserving
global-order-preserving(es;X;f) == \mforall{}a,a':E(X). (a is f*(a') {}\mRightarrow{} (\mforall{}b,b':E(X). (b is f*(b') {}\mRightarrow{} (loc(a) = loc(b)) {}\mRightarrow{} (loc(a') = loc(b')) {}\mRightarrow{} ((a <loc b) \mLeftarrow{}{}\mRightarrow{} (a' <loc b'))))) Date html generated: 2015_07_17-PM-00_58_36 Last ObjectModification: 2012_02_25-PM-01_31_15 Home Index