HSR(0,0)<=1 must be forbidden by the playground. If this claim is used, there is an exception thrown because the quality is 0. HSR(n,k) <= q is only allowed if n>0. -- Karl -------------- next part -------------- HTML attachment scrubbed and removed