Nuprl Definition : interface-order-preserving
interface-order-preserving(es;X;f) ==
∀e,e':E(X). ((loc(e) = loc(e') ∈ Id) ⇒ (loc(f e) = loc(f e') ∈ Id) ⇒ ((f e <loc f e') ⇐⇒ (e <loc e')))
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,
apply: f a,
equal: s = t ∈ T
FDL editor aliases :
interface-order-preserving
interface-order-preserving(es;X;f) ==
\mforall{}e,e':E(X). ((loc(e) = loc(e')) {}\mRightarrow{} (loc(f e) = loc(f e')) {}\mRightarrow{} ((f e <loc f e') \mLeftarrow{}{}\mRightarrow{} (e <loc e')))
Date html generated:
2015_07_17-PM-00_57_54
Last ObjectModification:
2012_02_25-PM-01_30_45
Home
Index