Nuprl Definition : pv11_p1_lt_bnum'
pv11_p1_lt_bnum'(ldrs_uid) ==
λzb,z. let i1,l1 = zb in let i2,l2 = z in i1 <z i2 ∨b((i1 =z i2) ∧b ldrs_uid l1 <z ldrs_uid l2)
Definitions occuring in Statement :
bor: p ∨bq,
band: p ∧b q,
lt_int: i <z j,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
spread: spread def
FDL editor aliases :
pv11_p1_lt_bnum'
Latex:
pv11\_p1\_lt\_bnum'(ldrs$_{uid}$) ==
\mlambda{}zb,z. let i1,l1 = zb in let i2,l2 = z in i1 <z i2 \mvee{}\msubb{}((i1 =\msubz{} i2) \mwedge{}\msubb{} ldrs$_{uid}\mbackslash{}ff\000C24 l1 <z ldrs$_{uid}$ l2)
Date html generated:
2015_07_23-PM-04_10_57
Last ObjectModification:
2014_11_26-AM-11_22_04
Home
Index