### Nuprl Definition : message-constraint2

`message-constraint2{i:l}(es;X;hdrs) ==`
`  ∀e1,e2:E.`
`    ((header(e1) ∈ hdrs)`
`    `` (header(e2) ∈ hdrs)`
`    `` single-valued-classrel(es;X;Id × Message{i:l})`
`    `` (¬(e1 = e2 ∈ E))`
`    `` (↓∃e1',e2':E`
`          ((e1' < e1) ∧ (e2' < e2) ∧ (¬(e1' = e2' ∈ E)) ∧ <loc(e1), info(e1)> ∈ X(e1') ∧ <loc(e2), info(e2)> ∈ X(e2'))))`

Definitions occuring in Statement :  es-header: `header(e)` single-valued-classrel: `single-valued-classrel(es;X;T)` classrel: `v ∈ X(e)` es-info: `info(e)` es-causl: `(e < e')` es-loc: `loc(e)` es-E: `E` Id: `Id` name: `Name` l_member: `(x ∈ l)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` squash: `↓T` implies: `P `` Q` and: `P ∧ Q` pair: `<a, b>` product: `x:A × B[x]` equal: `s = t ∈ T`
FDL editor aliases :  message-constraint2

Latex:
message-constraint2\{i:l\}(es;X;hdrs)  ==
\mforall{}e1,e2:E.
{}\mRightarrow{}  single-valued-classrel(es;X;Id  \mtimes{}  Message\{i:l\})
{}\mRightarrow{}  (\mneg{}(e1  =  e2))
{}\mRightarrow{}  (\mdownarrow{}\mexists{}e1',e2':E
((e1'  <  e1)
\mwedge{}  (e2'  <  e2)
\mwedge{}  (\mneg{}(e1'  =  e2'))
\mwedge{}  <loc(e1),  info(e1)>  \mmember{}  X(e1')
\mwedge{}  <loc(e2),  info(e2)>  \mmember{}  X(e2'))))

Date html generated: 2015_07_22-PM-00_15_33
Last ObjectModification: 2012_11_29-AM-11_15_35

Home Index