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