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.
((header(e1) \mmember{} hdrs)
{}\mRightarrow{} (header(e2) \mmember{} hdrs)
{}\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:
2016_05_17-AM-09_28_39
Last ObjectModification:
2012_11_29-AM-11_15_35
Theory : classrel!lemmas
Home
Index