Nuprl Definition : pv11_p1_leq_bnum

pv11_p1_leq_bnum(ldrs_uid) ==
  λbn1,bn2. case bn1
            of inl(x1) =>
            case bn2 of inl(x2) => pv11_p1_leq_bnum'(ldrs_uid) x1 x2 | inr(z) => ff
            | inr(z) =>
            tt


Definitions occuring in Statement :  pv11_p1_leq_bnum': pv11_p1_leq_bnum'(ldrs_uid),  bfalse: ff,  btrue: tt,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  pv11_p1_leq_bnum
Latex:
pv11\_p1\_leq\_bnum(ldrs$_{uid}$)  ==
    \mlambda{}bn1,bn2.  case  bn1
                        of  inl(x1)  =>
                        case  bn2  of  inl(x2)  =>  pv11\_p1\_leq\_bnum'(ldrs$_{uid}$)  x1  x2  |  inr(z\000C)  =>  ff
                        |  inr(z)  =>
                        tt


Date html generated: 2015_07_23-PM-04_10_55
Last ObjectModification: 2014_11_26-AM-11_22_00

Home Index