blob: d12077c7c23551ea98a135f59be415c73588cb43 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
symbolic N,M,k;
{ [i,j] -> [] : 0 <= i <= M and 0 <= j <= N and 2i+j = k
and not ( exists [i2,j2] :
0 <= i2 <= M and 0 <= j2 <= N
and 2i2+j2 = k
and i < i2 ) };
{ [i,j] -> [] : 0 <= i <= M and 0 <= j <= N and 2i+j = k
and not ( i < M && 2i-2 <= k &&
N-k <= 2M
&& ( N-k < k or N <= 2k && (exists a : k = 2 a)
))};
|
