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: 2016_05_16-PM-11_15_28 Last ObjectModification: 2012_02_25-PM-01_58_05 Theory : event-ordering Home Index