interface-fifo(es;X;f) ==
e,e':E(X). ((loc(e) = loc(e')) 
(f e <loc f e') (e <loc e'))
Definitions :
all: x:A. B[x],
es-E-interface: E(X),
equal: s = t,
Id: Id,
es-loc: loc(e),
implies: P Q,
apply: f a,
es-locl: (e <loc e')
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:
2010_08_27-PM-02_08_38
Last ObjectModification:
2009_12_16-AM-01_31_58
Home
Index