Blob Blame History Raw
{ S2[i, div36, div37, div38] -> [i, div36, k, div38, 1] : 3div37 = 2 + i and 3k = 2 + i and i >= 1 and i <= 10 and 3div36 >= -2 + i and 3div38 <= 1 + i and 3div38 >= -1 + i and 3div36 <= i; S1[i, div36, div37, div38] -> [i, j, div37, div38, 0] : 3j = i and 3div36 = i and i >= 3 and i <= 10 and 3div37 >= i and 3div38 <= 1 + i and 3div37 <= 2 + i and 3div38 >= -1 + i; S3[i, div36, div37, div38] -> [i, div36, div37, l, 2] : 3l = 1 + i and 3div38 = 1 + i and i <= 10 and i >= 2 and 3div36 >= -2 + i and 3div37 <= 2 + i and 3div36 <= i and 3div37 >= i; S4[i, div36, div37, div38] -> [i, div36, div37, div38, 3] : i >= 1 and i <= 10 and 3div36 <= i and 3div36 >= -2 + i and 3div37 <= 2 + i and 3div37 >= i and 3div38 <= 1 + i and 3div38 >= -1 + i }
{  :  }
{ [i, j, k, l, m] -> separate[o0] }