Nuprl Definition : pv11_p1_lt_bnum

pv11_p1_lt_bnum{ABS:q, paxos-v11-part1.esh:o}(ldrs_uid) ==
  λbn1,bn2. case bn1
            of inl(x1) =>
            case bn2 of inl(x2) => pv11_p1_lt_bnum'(ldrs_uid) x1 x2 | inr(z) => ff
            | inr(z) =>
            isl(bn2)


Definitions occuring in Statement :  pv11_p1_lt_bnum': pv11_p1_lt_bnum'(ldrs_uid),  isl: isl(x),  bfalse: ff,  apply: f a,  lambda: λx.A[x],  decide: case b of inl(x) => s[x] | inr(y) => t[y]
FDL editor aliases :  pv11_p1_lt_bnum
Latex:
pv11\_p1\_lt\_bnum\{ABS:q,  paxos-v11-part1.esh:o\}(ldrs$_{uid}$)  ==
    \mlambda{}bn1,bn2.  case  bn1
                        of  inl(x1)  =>
                        case  bn2  of  inl(x2)  =>  pv11\_p1\_lt\_bnum'(ldrs$_{uid}$)  x1  x2  |  inr(z)\000C  =>  ff
                        |  inr(z)  =>
                        isl(bn2)


Date html generated: 2016_05_17-PM-02_47_23
Last ObjectModification: 2015_05_14-PM-00_49_29

Theory : paxos!synod


Home Index