Nuprl Definition : pv8_p1_leq_bnum'
pv8_p1_leq_bnum'(ldrs_uid) ==
za.let i1,l1 = za
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 :
le_int: i z j,
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_leq_bnum'
pv8_p1_leq_bnum'
pv8\_p1\_leq\_bnum'(ldrs$_{uid}$) ==
\mlambda{}za.let i1,l1 = za
in \mlambda{}z.let i2,l2 = z
in i1 <z i2 \mvee{}\msubb{}((eqof(IntDeq) i1 i2) \mwedge{}\msubb{} ldrs$_{uid}$ l1 \mleq{}z ldrs$\mbackslash{}\000Cff5f{uid}$ l2)
Date html generated:
2012_02_20-PM-07_13_34
Last ObjectModification:
2012_02_06-PM-01_36_19
Home
Index