Nuprl Lemma : pax-p2a-type_wf
[es:EO']. [accpts:Id List]. (pax-p2a-type(es;accpts) 
')
Proof not projected
Definitions occuring in Statement :
pax-p2a-type: pax-p2a-type(es;accpts),
Message: Message,
event-ordering+: EO+(Info),
Id: Id,
uall: [x:A]. B[x],
prop: ,
member: t T,
list: type List
Definitions :
pax_p2a: pax_p2a(),
PValue: PValue(),
product: x:A 
B[x],
type-of-message: type-of-message(es;nm;locs;T),
function: x:A 
B[x],
all: x:A. B[x],
Message: Message,
prop: ,
universe: Type,
pax-p2a-type: pax-p2a-type(es;accpts),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
list: type List,
Id: Id,
member: t T,
equal: s = t,
event-ordering+: EO+(Info)
Lemmas :
event-ordering+_wf,
Message_wf,
Id_wf,
type-of-message_wf,
PValue_wf,
pax_p2a_wf
\mforall{}[es:EO']. \mforall{}[accpts:Id List]. (pax-p2a-type(es;accpts) \mmember{} \mBbbP{}')
Date html generated:
2011_10_20-PM-11_50_50
Last ObjectModification:
2011_05_24-PM-01_24_27
Home
Index