Nuprl Definition : fifo-information-flow
fifo-information-flow(es;T;S;F;In;X;f) ==
solves-information-flow(es;T;S;F;In;X;f)
∧ (∀e1,e2:E(X).
((¬((f e1) = e1 ∈ E(X)))
⇒ (¬((f e2) = e2 ∈ E(X)))
⇒ (f e1 <loc f e2)
⇒ (loc(e1) = loc(e2) ∈ Id)
⇒ (e1 <loc e2)))
Definitions occuring in Statement :
solves-information-flow: solves-information-flow(es;T;S;F;In;X;f)
,
es-E-interface: E(X)
,
es-locl: (e <loc e')
,
es-loc: loc(e)
,
Id: Id
,
all: ∀x:A. B[x]
,
not: ¬A
,
implies: P
⇒ Q
,
and: P ∧ Q
,
apply: f a
,
equal: s = t ∈ T
FDL editor aliases :
fifo-information-flow
Latex:
fifo-information-flow(es;T;S;F;In;X;f) ==
solves-information-flow(es;T;S;F;In;X;f)
\mwedge{} (\mforall{}e1,e2:E(X).
((\mneg{}((f e1) = e1))
{}\mRightarrow{} (\mneg{}((f e2) = e2))
{}\mRightarrow{} (f e1 <loc f e2)
{}\mRightarrow{} (loc(e1) = loc(e2))
{}\mRightarrow{} (e1 <loc e2)))
Date html generated:
2015_07_20-PM-03_54_40
Last ObjectModification:
2012_02_25-PM-01_58_05
Home
Index