Blob Blame History Raw
[M, N] -> { S1[i0, i1, i2, i3, i4, i2] -> [i0, i1, i2, i3, i4, i2] : 5i0 <= -7 + 2M + 2N and i4 >= i0 - i2 and 10i2 >= -2 - N + 5i0 and i2 >= -1 + i0 - i1 and 2i4 >= i0 and i0 >= 1 and i1 >= 1 and 2i1 >= i0 and i2 >= 0 and 5i2 >= 1 - M - N + 5i0 and 5i4 >= -1 - M + 5i0 and i3 >= i0 and 5i1 >= -2 - M + 5i0 and i3 >= 1 and 5i3 >= -3 - N + 5i1 + 5i2 and 5i2 <= 4 + N + 5i0 - 5i1 and i4 >= 1 and i2 <= i0 and 5i3 >= -2N + 10i1 and 5i1 <= -5 + M + 2N and 10i1 <= 1 + 2N + 5i0 and 5i2 >= -1 - N + 5i1 and i4 >= i1 and i3 >= i1 and i2 <= i1 and i1 <= i0 and 5i4 <= 4 + N - 5i2 + 5i3 and 5i4 <= 5 + N + 5i0 - 5i2 and 5i3 >= -2 - N + 10i2 and 5i2 <= -2 + M + N and 10i2 <= 3 + N + 5i0 and N >= 4 and i4 >= i2 and i3 >= i2 and M >= 3 and i4 <= i0 and 5i3 <= -6 + 2M + 2N and i4 >= -1 - i2 + i3 and 5i3 <= 3 + N + 10i2 and i3 <= 1 + i1 + i2 and i4 <= 1 + i1 and 2i4 >= i3 and 5i4 <= 2 + N + 5i2 and i3 <= 1 + 2i1 and i4 <= i3 and 5i3 <= M + N + 5i2 and 5i4 >= -2 - M + 5i3 and 10i4 <= 3 + 2N + 5i0 and i3 <= 1 + i0 and 5i3 <= 3 + M + 5i1 and 5i4 <= -4 + M + 2N and 10i4 <= 2 + 2N + 5i3 }
[M, N] -> {  : M >= 1 and N >= 1 }
[M, N] -> { [i, j, k, l, m, n] -> separate[o0] }