const int k;

// Anonymity - check for k=0..2^N - both min/max should be the same and equal to 1/2^(N-1) or 0
// (depending on the parity of the number of bits in the binary representation of outcome)
Pmin=? [ F "done" & outcome = k {"init"&pay>0}{min} ]
Pmax=? [ F "done" & outcome = k {"init"&pay>0}{max} ]