eval remark12b "?msd_fib ~Ei,p (p>0) & Au (u>=i & 3*u<=3*i+4*p) => W[u]=W[u+p]"::