Nuprl Definition : pax-p2a-msgs
pax-p2a-msgs{i:l}() == {m:Message| (msg-header(m) = pax_p2a()) 
(msg-type(m) 
r (Id 
PValue()))}
Proof not projected
Definitions occuring in Statement :
pax_p2a: pax_p2a(),
PValue: PValue(),
msg-header: msg-header(m),
msg-type: msg-type(msg),
Message: Message,
Id: Id,
name: Name,
subtype_rel: A r B,
and: P Q,
set: {x:A| B[x]} ,
product: x:A B[x],
equal: s = t
Definitions :
set: {x:A| B[x]} ,
Message: Message,
and: P Q,
equal: s = t,
name: Name,
msg-header: msg-header(m),
pax_p2a: pax_p2a(),
subtype_rel: A r B,
msg-type: msg-type(msg),
product: x:A B[x],
Id: Id,
PValue: PValue()
FDL editor aliases :
pax-p2a-msgs
pax-p2a-msgs\{i:l\}() == \{m:Message| (msg-header(m) = pax\_p2a()) \mwedge{} (msg-type(m) \msubseteq{}r (Id \mtimes{} PValue()))\}
Date html generated:
2011_10_20-PM-11_51_05
Last ObjectModification:
2011_05_25-PM-03_10_50
Home
Index