Nuprl Definition : pv8_p1_leq_bnum
pv8_p1_leq_bnum(ldrs_uid) ==
bn1,bn2.((
isl(bn1)) 
(isl(bn1) 
isl(bn2) (pv8_p1_leq_bnum'(ldrs_uid) outl(bn1) outl(bn2))))
Definitions occuring in Statement :
pv8_p1_leq_bnum': pv8_p1_leq_bnum'(ldrs_uid),
outl: outl(x),
isl: isl(x),
bor: p q,
band: p q,
bnot: b,
apply: f a,
lambda: x.A[x]
FDL editor aliases :
pv8_p1_leq_bnum
pv8_p1_leq_bnum
pv8\_p1\_leq\_bnum(ldrs$_{uid}$) ==
\mlambda{}bn1,bn2.
((\mneg{}\msubb{}isl(bn1)) \mvee{}\msubb{}(isl(bn1) \mwedge{}\msubb{} isl(bn2) \mwedge{}\msubb{} (pv8\_p1\_leq\_bnum'(ldrs$_{uid}$) outl\000C(bn1) outl(bn2))))
Date html generated:
2012_02_20-PM-07_13_47
Last ObjectModification:
2012_02_06-PM-01_36_29
Home
Index