Nuprl Definition : Paxos-spec8-spec713
Collect2 ==
  es-collect-filter-max(x1; x2 + 1; vs.fst(snd(vs)); vs.tt; vs.case snd(snd(vs)) of inl(p) => fst(p) | inr(x) => -1)
Definitions occuring in Statement : 
btrue: tt
, 
pi1: fst(t)
, 
pi2: snd(t)
, 
decide: case b of inl(x) => s[x] | inr(y) => t[y]
, 
add: n + m
, 
minus: -n
, 
natural_number: $n
Latex:
Collect2  ==
    es-collect-filter-max(x1;
                                                x2  +  1;
                                                vs.fst(snd(vs));
                                                vs.tt;
                                                vs.case  snd(snd(vs))  of  inl(p)  =>  fst(p)  |  inr(x)  =>  -1)
Date html generated:
2016_05_16-AM-10_53_07
Last ObjectModification:
2012_02_25-AM-10_52_07
Theory : event-ordering
Home
Index