Nuprl Definition : message-constraint-swap-hdr
message-constraint-swap-hdr{i:l}(f; es; X; hdr_in; hdrs_out) ==
∀e:E
((header(e) = hdr_in ∈ Name)
⇒ (↓∃e':E
∃hdr:Name
(((hdr ∈ hdrs_out) ∧ ((f hdr) = (f hdr_in) ∈ Type)) ∧ (e' < e) ∧ <loc(e), make-Msg(hdr;msgval(e))> ∈ X(e'))))
Definitions occuring in Statement :
make-Msg: make-Msg(hdr;val),
es-info-body: msgval(e),
es-header: header(e),
Message: Message(f),
classrel: v ∈ X(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],
squash: ↓T,
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
pair: <a, b>,
product: x:A × B[x],
universe: Type,
equal: s = t ∈ T
Latex:
message-constraint-swap-hdr\{i:l\}(f; es; X; hdr$_{in}$; hdrs$_{out\mbackslash{}ff\000C7d$) ==
\mforall{}e:E
((header(e) = hdr$_{in}$)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
\mexists{}hdr:Name
(((hdr \mmember{} hdrs$_{out}$) \mwedge{} ((f hdr) = (f hdr$_{in}$\000C)))
\mwedge{} (e' < e)
\mwedge{} <loc(e), make-Msg(hdr;msgval(e))> \mmember{} X(e'))))
Date html generated:
2015_07_21-PM-04_53_58
Last ObjectModification:
2013_02_26-PM-01_04_36
Home
Index