Nuprl Definition : pv8_p1_lt_bnum
pv8_p1_lt_bnum(ldrs_uid) ==
bn1,bn2.(((
isl(bn1)) 
isl(bn2)) 
(isl(bn1) isl(bn2) (pv8_p1_lt_bnum'(ldrs_uid) outl(bn1) outl(bn2))))
Definitions occuring in Statement :
pv8_p1_lt_bnum': pv8_p1_lt_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_lt_bnum
pv8_p1_lt_bnum
pv8\_p1\_lt\_bnum(ldrs$_{uid}$) ==
\mlambda{}bn1,bn2.
(((\mneg{}\msubb{}isl(bn1)) \mwedge{}\msubb{} isl(bn2))
\mvee{}\msubb{}(isl(bn1) \mwedge{}\msubb{} isl(bn2) \mwedge{}\msubb{} (pv8\_p1\_lt\_bnum'(ldrs$_{uid}$) outl(bn1) outl(bn2)\000C)))
Date html generated:
2012_02_20-PM-07_14_14
Last ObjectModification:
2012_02_06-PM-01_36_50
Home
Index