Nuprl Definition : pv11_p1_leq_bnum'
pv11_p1_leq_bnum'(ldrs_uid) ==
λza,z. let i1,l1 = za 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 :
le_int: i ≤z j,
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_leq_bnum'
Latex:
pv11\_p1\_leq\_bnum'(ldrs$_{uid}$) ==
\mlambda{}za,z. let i1,l1 = za in let i2,l2 = z in i1 <z i2 \mvee{}\msubb{}((i1 =\msubz{} i2) \mwedge{}\msubb{} ldrs$_{uid}\mbackslash{}ff\000C24 l1 \mleq{}z ldrs$_{uid}$ l2)
Date html generated:
2015_07_23-PM-04_10_53
Last ObjectModification:
2014_11_26-AM-11_21_57
Home
Index