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
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:
2015_07_17-AM-09_10_47
Last ObjectModification:
2012_02_25-AM-10_52_07
Home
Index