Nuprl Definition : pv8_p1_lt_bnum'
pv8_p1_lt_bnum'(ldrs_uid) ==
zb.let i1,l1 = zb
in z.let i2,l2 = z
in i1 <z i2 
((eqof(IntDeq) i1 i2) 
ldrs_uid l1 <z ldrs_uid l2)
Definitions occuring in Statement :
bor: p q,
band: p q,
lt_int: i <z j,
apply: f a,
lambda: x.A[x],
spread: spread def,
int-deq: IntDeq,
eqof: eqof(d)
FDL editor aliases :
pv8_p1_lt_bnum'
pv8_p1_lt_bnum'
pv8\_p1\_lt\_bnum'(ldrs$_{uid}$) ==
\mlambda{}zb.let i1,l1 = zb
in \mlambda{}z.let i2,l2 = z
in i1 <z i2 \mvee{}\msubb{}((eqof(IntDeq) i1 i2) \mwedge{}\msubb{} ldrs$_{uid}$ l1 <z ldrs$\mbackslash{}\000Cff5f{uid}$ l2)
Date html generated:
2012_02_20-PM-07_14_01
Last ObjectModification:
2012_02_06-PM-01_36_39
Home
Index