Nuprl Definition : pax-p2a-msgs'
pax-p2a-msgs'{i:l}() == {m:Message| (msg-header(m) = pax_p2a()) 
(
msg-type(m) == 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,
assert: b,
and: P Q,
set: {x:A| B[x]} ,
product: x:A B[x],
equal: s = t,
eq_term: a == b
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(),
assert: b,
eq_term: a == 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{} (\muparrow{}msg-type(m) == Id \mtimes{} PValue())\}
Date html generated:
2011_10_20-PM-11_51_35
Last ObjectModification:
2011_05_25-PM-04_05_15
Home
Index